Proof of Theorem oeoe
Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) = (∅ ↑𝑜
∅)) |
2 | | oe0m0 7600 |
. . . . . . . . . . . 12
⊢ (∅
↑𝑜 ∅) = 1𝑜 |
3 | 1, 2 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) = 1𝑜) |
4 | 3 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝐵 = ∅ → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (1𝑜
↑𝑜 𝐶)) |
5 | | oe1m 7625 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On →
(1𝑜 ↑𝑜 𝐶) = 1𝑜) |
6 | 4, 5 | sylan9eqr 2678 |
. . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ 𝐵 = ∅) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) =
1𝑜) |
7 | 6 | adantll 750 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐵 = ∅) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) =
1𝑜) |
8 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝐶 = ∅ → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = ((∅
↑𝑜 𝐵) ↑𝑜
∅)) |
9 | | 0elon 5778 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
10 | | oecl 7617 |
. . . . . . . . . . . 12
⊢ ((∅
∈ On ∧ 𝐵 ∈
On) → (∅ ↑𝑜 𝐵) ∈ On) |
11 | 9, 10 | mpan 706 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → (∅
↑𝑜 𝐵) ∈ On) |
12 | | oe0 7602 |
. . . . . . . . . . 11
⊢ ((∅
↑𝑜 𝐵) ∈ On → ((∅
↑𝑜 𝐵) ↑𝑜 ∅) =
1𝑜) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → ((∅
↑𝑜 𝐵) ↑𝑜 ∅) =
1𝑜) |
14 | 8, 13 | sylan9eqr 2678 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 = ∅) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) =
1𝑜) |
15 | 14 | adantlr 751 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐶 = ∅) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) =
1𝑜) |
16 | 7, 15 | jaodan 826 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) =
1𝑜) |
17 | | om00 7655 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 ·𝑜
𝐶) = ∅ ↔ (𝐵 = ∅ ∨ 𝐶 = ∅))) |
18 | 17 | biimpar 502 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → (𝐵 ·𝑜
𝐶) =
∅) |
19 | 18 | oveq2d 6666 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → (∅
↑𝑜 (𝐵 ·𝑜 𝐶)) = (∅
↑𝑜 ∅)) |
20 | 19, 2 | syl6eq 2672 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → (∅
↑𝑜 (𝐵 ·𝑜 𝐶)) =
1𝑜) |
21 | 16, 20 | eqtr4d 2659 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶))) |
22 | | on0eln0 5780 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
23 | | on0eln0 5780 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
24 | 22, 23 | bi2anan9 917 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) ↔ (𝐵 ≠ ∅ ∧ 𝐶 ≠
∅))) |
25 | | neanior 2886 |
. . . . . . . . 9
⊢ ((𝐵 ≠ ∅ ∧ 𝐶 ≠ ∅) ↔ ¬
(𝐵 = ∅ ∨ 𝐶 = ∅)) |
26 | 24, 25 | syl6bb 276 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) ↔ ¬
(𝐵 = ∅ ∨ 𝐶 = ∅))) |
27 | | oe0m1 7601 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
28 | 27 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) = ∅) |
29 | 28 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 𝐶)) |
30 | | oe0m1 7601 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ (∅
↑𝑜 𝐶) = ∅)) |
31 | 30 | biimpa 501 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ On ∧ ∅ ∈
𝐶) → (∅
↑𝑜 𝐶) = ∅) |
32 | 29, 31 | sylan9eq 2676 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ ∅ ∈
𝐵) ∧ (𝐶 ∈ On ∧ ∅ ∈ 𝐶)) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = ∅) |
33 | 32 | an4s 869 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∧ ∅
∈ 𝐶)) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = ∅) |
34 | | om00el 7656 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
·𝑜 𝐶) ↔ (∅ ∈ 𝐵 ∧ ∅ ∈ 𝐶))) |
35 | | omcl 7616 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ·𝑜
𝐶) ∈
On) |
36 | | oe0m1 7601 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ·𝑜
𝐶) ∈ On →
(∅ ∈ (𝐵
·𝑜 𝐶) ↔ (∅ ↑𝑜
(𝐵
·𝑜 𝐶)) = ∅)) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
·𝑜 𝐶) ↔ (∅ ↑𝑜
(𝐵
·𝑜 𝐶)) = ∅)) |
38 | 34, 37 | bitr3d 270 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) ↔ (∅
↑𝑜 (𝐵 ·𝑜 𝐶)) = ∅)) |
39 | 38 | biimpa 501 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∧ ∅
∈ 𝐶)) → (∅
↑𝑜 (𝐵 ·𝑜 𝐶)) = ∅) |
40 | 33, 39 | eqtr4d 2659 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∧ ∅
∈ 𝐶)) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶))) |
41 | 40 | ex 450 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶)))) |
42 | 26, 41 | sylbird 250 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (¬ (𝐵 = ∅ ∨ 𝐶 = ∅) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶)))) |
43 | 42 | imp 445 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ¬ (𝐵 = ∅ ∨ 𝐶 = ∅)) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶))) |
44 | 21, 43 | pm2.61dan 832 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶))) |
45 | | oveq1 6657 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
46 | 45 | oveq1d 6665 |
. . . . . 6
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = ((∅ ↑𝑜
𝐵)
↑𝑜 𝐶)) |
47 | | oveq1 6657 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
(𝐵
·𝑜 𝐶)) = (∅ ↑𝑜
(𝐵
·𝑜 𝐶))) |
48 | 46, 47 | eqeq12d 2637 |
. . . . 5
⊢ (𝐴 = ∅ → (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶)) ↔ ((∅
↑𝑜 𝐵) ↑𝑜 𝐶) = (∅
↑𝑜 (𝐵 ·𝑜 𝐶)))) |
49 | 44, 48 | syl5ibr 236 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶)))) |
50 | 49 | impcom 446 |
. . 3
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐴 = ∅) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |
51 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ↑𝑜
𝐵) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵)) |
52 | 51 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ↑𝑜 𝐶)) |
53 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ↑𝑜
(𝐵
·𝑜 𝐶)) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 ·𝑜 𝐶))) |
54 | 52, 53 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶)) ↔ ((if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ↑𝑜 𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 ·𝑜 𝐶)))) |
55 | 54 | imbi2d 330 |
. . . . . 6
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) ↔ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ↑𝑜 𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 ·𝑜 𝐶))))) |
56 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ∈ On ↔ if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜) ∈
On)) |
57 | | eleq2 2690 |
. . . . . . . . . 10
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (∅
∈ 𝐴 ↔ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1𝑜))) |
58 | 56, 57 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) ↔ (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜) ∈ On ∧
∅ ∈ if((𝐴 ∈
On ∧ ∅ ∈ 𝐴),
𝐴,
1𝑜)))) |
59 | | eleq1 2689 |
. . . . . . . . . 10
⊢
(1𝑜 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) →
(1𝑜 ∈ On ↔ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) ∈
On)) |
60 | | eleq2 2690 |
. . . . . . . . . 10
⊢
(1𝑜 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (∅
∈ 1𝑜 ↔ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜))) |
61 | 59, 60 | anbi12d 747 |
. . . . . . . . 9
⊢
(1𝑜 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) →
((1𝑜 ∈ On ∧ ∅ ∈ 1𝑜)
↔ (if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴, 1𝑜)
∈ On ∧ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)))) |
62 | | 1on 7567 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
63 | | 0lt1o 7584 |
. . . . . . . . . 10
⊢ ∅
∈ 1𝑜 |
64 | 62, 63 | pm3.2i 471 |
. . . . . . . . 9
⊢
(1𝑜 ∈ On ∧ ∅ ∈
1𝑜) |
65 | 58, 61, 64 | elimhyp 4146 |
. . . . . . . 8
⊢
(if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴, 1𝑜)
∈ On ∧ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)) |
66 | 65 | simpli 474 |
. . . . . . 7
⊢ if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜) ∈
On |
67 | 65 | simpri 478 |
. . . . . . 7
⊢ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1𝑜) |
68 | 66, 67 | oeoelem 7678 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ↑𝑜 𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 ·𝑜 𝐶))) |
69 | 55, 68 | dedth 4139 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶)))) |
70 | 69 | imp 445 |
. . . 4
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) → ((𝐴 ↑𝑜 𝐵) ↑𝑜
𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |
71 | 70 | an32s 846 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) ∧ ∅
∈ 𝐴) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |
72 | 50, 71 | oe0lem 7593 |
. 2
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |
73 | 72 | 3impb 1260 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜
𝐵)
↑𝑜 𝐶) = (𝐴 ↑𝑜 (𝐵 ·𝑜
𝐶))) |