Proof of Theorem oeoa
Step | Hyp | Ref
| Expression |
1 | | oa00 7639 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 +𝑜 𝐶) = ∅ ↔ (𝐵 = ∅ ∧ 𝐶 = ∅))) |
2 | 1 | biimpar 502 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∧ 𝐶 = ∅)) → (𝐵 +𝑜 𝐶) = ∅) |
3 | 2 | oveq2d 6666 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∧ 𝐶 = ∅)) → (∅
↑𝑜 (𝐵 +𝑜 𝐶)) = (∅ ↑𝑜
∅)) |
4 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) = (∅ ↑𝑜
∅)) |
5 | | oveq2 6658 |
. . . . . . . . . . 11
⊢ (𝐶 = ∅ → (∅
↑𝑜 𝐶) = (∅ ↑𝑜
∅)) |
6 | | oe0m0 7600 |
. . . . . . . . . . 11
⊢ (∅
↑𝑜 ∅) = 1𝑜 |
7 | 5, 6 | syl6eq 2672 |
. . . . . . . . . 10
⊢ (𝐶 = ∅ → (∅
↑𝑜 𝐶) = 1𝑜) |
8 | 4, 7 | oveqan12d 6669 |
. . . . . . . . 9
⊢ ((𝐵 = ∅ ∧ 𝐶 = ∅) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ((∅ ↑𝑜
∅) ·𝑜 1𝑜)) |
9 | | 0elon 5778 |
. . . . . . . . . . 11
⊢ ∅
∈ On |
10 | | oecl 7617 |
. . . . . . . . . . 11
⊢ ((∅
∈ On ∧ ∅ ∈ On) → (∅ ↑𝑜
∅) ∈ On) |
11 | 9, 9, 10 | mp2an 708 |
. . . . . . . . . 10
⊢ (∅
↑𝑜 ∅) ∈ On |
12 | | om1 7622 |
. . . . . . . . . 10
⊢ ((∅
↑𝑜 ∅) ∈ On → ((∅
↑𝑜 ∅) ·𝑜
1𝑜) = (∅ ↑𝑜
∅)) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . 9
⊢ ((∅
↑𝑜 ∅) ·𝑜
1𝑜) = (∅ ↑𝑜
∅) |
14 | 8, 13 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝐵 = ∅ ∧ 𝐶 = ∅) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = (∅ ↑𝑜
∅)) |
15 | 14 | adantl 482 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∧ 𝐶 = ∅)) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = (∅ ↑𝑜
∅)) |
16 | 3, 15 | eqtr4d 2659 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∧ 𝐶 = ∅)) → (∅
↑𝑜 (𝐵 +𝑜 𝐶)) = ((∅ ↑𝑜
𝐵)
·𝑜 (∅ ↑𝑜 𝐶))) |
17 | | oacl 7615 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 +𝑜 𝐶) ∈ On) |
18 | | on0eln0 5780 |
. . . . . . . . . 10
⊢ ((𝐵 +𝑜 𝐶) ∈ On → (∅
∈ (𝐵
+𝑜 𝐶)
↔ (𝐵
+𝑜 𝐶)
≠ ∅)) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
+𝑜 𝐶)
↔ (𝐵
+𝑜 𝐶)
≠ ∅)) |
20 | | oe0m1 7601 |
. . . . . . . . . 10
⊢ ((𝐵 +𝑜 𝐶) ∈ On → (∅
∈ (𝐵
+𝑜 𝐶)
↔ (∅ ↑𝑜 (𝐵 +𝑜 𝐶)) = ∅)) |
21 | 17, 20 | syl 17 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
+𝑜 𝐶)
↔ (∅ ↑𝑜 (𝐵 +𝑜 𝐶)) = ∅)) |
22 | 1 | necon3abid 2830 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 +𝑜 𝐶) ≠ ∅ ↔ ¬
(𝐵 = ∅ ∧ 𝐶 = ∅))) |
23 | 19, 21, 22 | 3bitr3d 298 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
↑𝑜 (𝐵 +𝑜 𝐶)) = ∅ ↔ ¬ (𝐵 = ∅ ∧ 𝐶 = ∅))) |
24 | 23 | biimpar 502 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ¬ (𝐵 = ∅ ∧ 𝐶 = ∅)) → (∅
↑𝑜 (𝐵 +𝑜 𝐶)) = ∅) |
25 | | on0eln0 5780 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
26 | 25 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
27 | | on0eln0 5780 |
. . . . . . . . . . . 12
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
28 | 27 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
29 | 26, 28 | orbi12d 746 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∨ ∅
∈ 𝐶) ↔ (𝐵 ≠ ∅ ∨ 𝐶 ≠
∅))) |
30 | | neorian 2888 |
. . . . . . . . . 10
⊢ ((𝐵 ≠ ∅ ∨ 𝐶 ≠ ∅) ↔ ¬
(𝐵 = ∅ ∧ 𝐶 = ∅)) |
31 | 29, 30 | syl6bb 276 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∨ ∅
∈ 𝐶) ↔ ¬
(𝐵 = ∅ ∧ 𝐶 = ∅))) |
32 | | oe0m1 7601 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
33 | 32 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑𝑜 𝐵) = ∅) |
34 | 33 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = (∅ ·𝑜
(∅ ↑𝑜 𝐶))) |
35 | | oecl 7617 |
. . . . . . . . . . . . . . 15
⊢ ((∅
∈ On ∧ 𝐶 ∈
On) → (∅ ↑𝑜 𝐶) ∈ On) |
36 | 9, 35 | mpan 706 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ On → (∅
↑𝑜 𝐶) ∈ On) |
37 | | om0r 7619 |
. . . . . . . . . . . . . 14
⊢ ((∅
↑𝑜 𝐶) ∈ On → (∅
·𝑜 (∅ ↑𝑜 𝐶)) = ∅) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ On → (∅
·𝑜 (∅ ↑𝑜 𝐶)) = ∅) |
39 | 34, 38 | sylan9eq 2676 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ On ∧ ∅ ∈
𝐵) ∧ 𝐶 ∈ On) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅) |
40 | 39 | an32s 846 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐵) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅) |
41 | | oe0m1 7601 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ (∅
↑𝑜 𝐶) = ∅)) |
42 | 41 | biimpa 501 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ∈ On ∧ ∅ ∈
𝐶) → (∅
↑𝑜 𝐶) = ∅) |
43 | 42 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ On ∧ ∅ ∈
𝐶) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ((∅ ↑𝑜
𝐵)
·𝑜 ∅)) |
44 | | oecl 7617 |
. . . . . . . . . . . . . . 15
⊢ ((∅
∈ On ∧ 𝐵 ∈
On) → (∅ ↑𝑜 𝐵) ∈ On) |
45 | 9, 44 | mpan 706 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
↑𝑜 𝐵) ∈ On) |
46 | | om0 7597 |
. . . . . . . . . . . . . 14
⊢ ((∅
↑𝑜 𝐵) ∈ On → ((∅
↑𝑜 𝐵) ·𝑜 ∅) =
∅) |
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ On → ((∅
↑𝑜 𝐵) ·𝑜 ∅) =
∅) |
48 | 43, 47 | sylan9eqr 2678 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ (𝐶 ∈ On ∧ ∅ ∈
𝐶)) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅) |
49 | 48 | anassrs 680 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅) |
50 | 40, 49 | jaodan 826 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∨ ∅
∈ 𝐶)) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅) |
51 | 50 | ex 450 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∨ ∅
∈ 𝐶) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅)) |
52 | 31, 51 | sylbird 250 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (¬ (𝐵 = ∅ ∧ 𝐶 = ∅) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅)) |
53 | 52 | imp 445 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ¬ (𝐵 = ∅ ∧ 𝐶 = ∅)) → ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶)) = ∅) |
54 | 24, 53 | eqtr4d 2659 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ¬ (𝐵 = ∅ ∧ 𝐶 = ∅)) → (∅
↑𝑜 (𝐵 +𝑜 𝐶)) = ((∅ ↑𝑜
𝐵)
·𝑜 (∅ ↑𝑜 𝐶))) |
55 | 16, 54 | pm2.61dan 832 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
↑𝑜 (𝐵 +𝑜 𝐶)) = ((∅ ↑𝑜
𝐵)
·𝑜 (∅ ↑𝑜 𝐶))) |
56 | | oveq1 6657 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = (∅
↑𝑜 (𝐵 +𝑜 𝐶))) |
57 | | oveq1 6657 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
58 | | oveq1 6657 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐶) = (∅
↑𝑜 𝐶)) |
59 | 57, 58 | oveq12d 6668 |
. . . . . 6
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝐶)) = ((∅
↑𝑜 𝐵) ·𝑜 (∅
↑𝑜 𝐶))) |
60 | 56, 59 | eqeq12d 2637 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶)) ↔ (∅
↑𝑜 (𝐵 +𝑜 𝐶)) = ((∅ ↑𝑜
𝐵)
·𝑜 (∅ ↑𝑜 𝐶)))) |
61 | 55, 60 | syl5ibr 236 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶)))) |
62 | 61 | impcom 446 |
. . 3
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐴 = ∅) → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |
63 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 +𝑜 𝐶))) |
64 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ↑𝑜
𝐵) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵)) |
65 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ↑𝑜
𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶)) |
66 | 64, 65 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → ((𝐴 ↑𝑜
𝐵)
·𝑜 (𝐴 ↑𝑜 𝐶)) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶))) |
67 | 63, 66 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → ((𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶)) ↔ (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 +𝑜 𝐶)) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶)))) |
68 | 67 | imbi2d 330 |
. . . . . 6
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → ((𝐶 ∈ On → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) ↔ (𝐶 ∈ On → (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 +𝑜 𝐶)) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶))))) |
69 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝐵 = if(𝐵 ∈ On, 𝐵, 1𝑜) → (𝐵 +𝑜 𝐶) = (if(𝐵 ∈ On, 𝐵, 1𝑜)
+𝑜 𝐶)) |
70 | 69 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ On, 𝐵, 1𝑜) → (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 +𝑜 𝐶)) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (if(𝐵 ∈ On, 𝐵, 1𝑜)
+𝑜 𝐶))) |
71 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝐵 = if(𝐵 ∈ On, 𝐵, 1𝑜) → (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 if(𝐵 ∈ On, 𝐵, 1𝑜))) |
72 | 71 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝐵 = if(𝐵 ∈ On, 𝐵, 1𝑜) → ((if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶)) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 if(𝐵 ∈ On, 𝐵, 1𝑜))
·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶))) |
73 | 70, 72 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ On, 𝐵, 1𝑜) → ((if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 +𝑜 𝐶)) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶)) ↔ (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (if(𝐵 ∈ On, 𝐵, 1𝑜)
+𝑜 𝐶)) =
((if((𝐴 ∈ On ∧
∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 if(𝐵 ∈ On, 𝐵, 1𝑜))
·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶)))) |
74 | 73 | imbi2d 330 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ On, 𝐵, 1𝑜) → ((𝐶 ∈ On → (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 (𝐵 +𝑜 𝐶)) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐵) ·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶))) ↔ (𝐶 ∈ On → (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 (if(𝐵 ∈ On, 𝐵, 1𝑜)
+𝑜 𝐶)) =
((if((𝐴 ∈ On ∧
∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 if(𝐵 ∈ On, 𝐵, 1𝑜))
·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶))))) |
75 | | eleq1 2689 |
. . . . . . . . . 10
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (𝐴 ∈ On ↔ if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜) ∈
On)) |
76 | | eleq2 2690 |
. . . . . . . . . 10
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (∅
∈ 𝐴 ↔ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1𝑜))) |
77 | 75, 76 | anbi12d 747 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → ((𝐴 ∈ On ∧ ∅ ∈
𝐴) ↔ (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜) ∈ On ∧
∅ ∈ if((𝐴 ∈
On ∧ ∅ ∈ 𝐴),
𝐴,
1𝑜)))) |
78 | | eleq1 2689 |
. . . . . . . . . 10
⊢
(1𝑜 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) →
(1𝑜 ∈ On ↔ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) ∈
On)) |
79 | | eleq2 2690 |
. . . . . . . . . 10
⊢
(1𝑜 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) → (∅
∈ 1𝑜 ↔ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜))) |
80 | 78, 79 | anbi12d 747 |
. . . . . . . . 9
⊢
(1𝑜 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜) →
((1𝑜 ∈ On ∧ ∅ ∈ 1𝑜)
↔ (if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴, 1𝑜)
∈ On ∧ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)))) |
81 | | 1on 7567 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
82 | | 0lt1o 7584 |
. . . . . . . . . 10
⊢ ∅
∈ 1𝑜 |
83 | 81, 82 | pm3.2i 471 |
. . . . . . . . 9
⊢
(1𝑜 ∈ On ∧ ∅ ∈
1𝑜) |
84 | 77, 80, 83 | elimhyp 4146 |
. . . . . . . 8
⊢
(if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴, 1𝑜)
∈ On ∧ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)) |
85 | 84 | simpli 474 |
. . . . . . 7
⊢ if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜) ∈
On |
86 | 84 | simpri 478 |
. . . . . . 7
⊢ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1𝑜) |
87 | 81 | elimel 4150 |
. . . . . . 7
⊢ if(𝐵 ∈ On, 𝐵, 1𝑜) ∈
On |
88 | 85, 86, 87 | oeoalem 7676 |
. . . . . 6
⊢ (𝐶 ∈ On → (if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1𝑜)
↑𝑜 (if(𝐵 ∈ On, 𝐵, 1𝑜)
+𝑜 𝐶)) =
((if((𝐴 ∈ On ∧
∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 if(𝐵 ∈ On, 𝐵, 1𝑜))
·𝑜 (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1𝑜)
↑𝑜 𝐶))) |
89 | 68, 74, 88 | dedth2h 4140 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ 𝐵 ∈ On) → (𝐶 ∈ On → (𝐴 ↑𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶)))) |
90 | 89 | impr 649 |
. . . 4
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) → (𝐴 ↑𝑜 (𝐵 +𝑜 𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |
91 | 90 | an32s 846 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) ∧ ∅
∈ 𝐴) → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |
92 | 62, 91 | oe0lem 7593 |
. 2
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |
93 | 92 | 3impb 1260 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜
(𝐵 +𝑜
𝐶)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
(𝐴
↑𝑜 𝐶))) |