Proof of Theorem oeoe
| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝐵 = ∅ → (∅
↑o 𝐵) =
(∅ ↑o ∅)) |
| 2 | | oe0m0 8558 |
. . . . . . . . . . . 12
⊢ (∅
↑o ∅) = 1o |
| 3 | 1, 2 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝐵 = ∅ → (∅
↑o 𝐵) =
1o) |
| 4 | 3 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝐵 = ∅ → ((∅
↑o 𝐵)
↑o 𝐶) =
(1o ↑o 𝐶)) |
| 5 | | oe1m 8583 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → (1o
↑o 𝐶) =
1o) |
| 6 | 4, 5 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝐶 ∈ On ∧ 𝐵 = ∅) → ((∅
↑o 𝐵)
↑o 𝐶) =
1o) |
| 7 | 6 | adantll 714 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐵 = ∅) → ((∅
↑o 𝐵)
↑o 𝐶) =
1o) |
| 8 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝐶 = ∅ → ((∅
↑o 𝐵)
↑o 𝐶) =
((∅ ↑o 𝐵) ↑o
∅)) |
| 9 | | 0elon 6438 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
| 10 | | oecl 8575 |
. . . . . . . . . . . 12
⊢ ((∅
∈ On ∧ 𝐵 ∈
On) → (∅ ↑o 𝐵) ∈ On) |
| 11 | 9, 10 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → (∅
↑o 𝐵)
∈ On) |
| 12 | | oe0 8560 |
. . . . . . . . . . 11
⊢ ((∅
↑o 𝐵)
∈ On → ((∅ ↑o 𝐵) ↑o ∅) =
1o) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → ((∅
↑o 𝐵)
↑o ∅) = 1o) |
| 14 | 8, 13 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 = ∅) → ((∅
↑o 𝐵)
↑o 𝐶) =
1o) |
| 15 | 14 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐶 = ∅) → ((∅
↑o 𝐵)
↑o 𝐶) =
1o) |
| 16 | 7, 15 | jaodan 960 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → ((∅
↑o 𝐵)
↑o 𝐶) =
1o) |
| 17 | | om00 8613 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 ·o 𝐶) = ∅ ↔ (𝐵 = ∅ ∨ 𝐶 = ∅))) |
| 18 | 17 | biimpar 477 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → (𝐵 ·o 𝐶) = ∅) |
| 19 | 18 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → (∅
↑o (𝐵
·o 𝐶)) =
(∅ ↑o ∅)) |
| 20 | 19, 2 | eqtrdi 2793 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → (∅
↑o (𝐵
·o 𝐶)) =
1o) |
| 21 | 16, 20 | eqtr4d 2780 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (𝐵 = ∅ ∨ 𝐶 = ∅)) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o (𝐵 ·o 𝐶))) |
| 22 | | on0eln0 6440 |
. . . . . . . . . 10
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ 𝐵 ≠ ∅)) |
| 23 | | on0eln0 6440 |
. . . . . . . . . 10
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
| 24 | 22, 23 | bi2anan9 638 |
. . . . . . . . 9
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) ↔ (𝐵 ≠ ∅ ∧ 𝐶 ≠
∅))) |
| 25 | | neanior 3035 |
. . . . . . . . 9
⊢ ((𝐵 ≠ ∅ ∧ 𝐶 ≠ ∅) ↔ ¬
(𝐵 = ∅ ∨ 𝐶 = ∅)) |
| 26 | 24, 25 | bitrdi 287 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) ↔ ¬
(𝐵 = ∅ ∨ 𝐶 = ∅))) |
| 27 | | oe0m1 8559 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
| 28 | 27 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → (∅
↑o 𝐵) =
∅) |
| 29 | 28 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ ∅ ∈
𝐵) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o 𝐶)) |
| 30 | | oe0m1 8559 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ On → (∅
∈ 𝐶 ↔ (∅
↑o 𝐶) =
∅)) |
| 31 | 30 | biimpa 476 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ On ∧ ∅ ∈
𝐶) → (∅
↑o 𝐶) =
∅) |
| 32 | 29, 31 | sylan9eq 2797 |
. . . . . . . . . . 11
⊢ (((𝐵 ∈ On ∧ ∅ ∈
𝐵) ∧ (𝐶 ∈ On ∧ ∅ ∈ 𝐶)) → ((∅
↑o 𝐵)
↑o 𝐶) =
∅) |
| 33 | 32 | an4s 660 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∧ ∅
∈ 𝐶)) → ((∅
↑o 𝐵)
↑o 𝐶) =
∅) |
| 34 | | om00el 8614 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
·o 𝐶)
↔ (∅ ∈ 𝐵
∧ ∅ ∈ 𝐶))) |
| 35 | | omcl 8574 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ·o 𝐶) ∈ On) |
| 36 | | oe0m1 8559 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ·o 𝐶) ∈ On → (∅
∈ (𝐵
·o 𝐶)
↔ (∅ ↑o (𝐵 ·o 𝐶)) = ∅)) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (∅
∈ (𝐵
·o 𝐶)
↔ (∅ ↑o (𝐵 ·o 𝐶)) = ∅)) |
| 38 | 34, 37 | bitr3d 281 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) ↔ (∅
↑o (𝐵
·o 𝐶)) =
∅)) |
| 39 | 38 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∧ ∅
∈ 𝐶)) → (∅
↑o (𝐵
·o 𝐶)) =
∅) |
| 40 | 33, 39 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ (∅
∈ 𝐵 ∧ ∅
∈ 𝐶)) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o (𝐵 ·o 𝐶))) |
| 41 | 40 | ex 412 |
. . . . . . . 8
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
∈ 𝐵 ∧ ∅
∈ 𝐶) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o (𝐵 ·o 𝐶)))) |
| 42 | 26, 41 | sylbird 260 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (¬ (𝐵 = ∅ ∨ 𝐶 = ∅) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o (𝐵 ·o 𝐶)))) |
| 43 | 42 | imp 406 |
. . . . . 6
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ¬ (𝐵 = ∅ ∨ 𝐶 = ∅)) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o (𝐵 ·o 𝐶))) |
| 44 | 21, 43 | pm2.61dan 813 |
. . . . 5
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((∅
↑o 𝐵)
↑o 𝐶) =
(∅ ↑o (𝐵 ·o 𝐶))) |
| 45 | | oveq1 7438 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
| 46 | 45 | oveq1d 7446 |
. . . . . 6
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝐵) ↑o 𝐶) = ((∅ ↑o
𝐵) ↑o 𝐶)) |
| 47 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ↑o (𝐵 ·o 𝐶)) = (∅ ↑o
(𝐵 ·o
𝐶))) |
| 48 | 46, 47 | eqeq12d 2753 |
. . . . 5
⊢ (𝐴 = ∅ → (((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶)) ↔ ((∅ ↑o 𝐵) ↑o 𝐶) = (∅ ↑o
(𝐵 ·o
𝐶)))) |
| 49 | 44, 48 | imbitrrid 246 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶)))) |
| 50 | 49 | impcom 407 |
. . 3
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ 𝐴 = ∅) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶))) |
| 51 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (𝐴 ↑o 𝐵) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o 𝐵)) |
| 52 | 51 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o 𝐵) ↑o 𝐶)) |
| 53 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (𝐴 ↑o (𝐵 ·o 𝐶)) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o (𝐵 ·o 𝐶))) |
| 54 | 52, 53 | eqeq12d 2753 |
. . . . . . 7
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶)) ↔ ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o 𝐵) ↑o 𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o (𝐵 ·o 𝐶)))) |
| 55 | 54 | imbi2d 340 |
. . . . . 6
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶))) ↔ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o 𝐵) ↑o 𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o (𝐵 ·o 𝐶))))) |
| 56 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (𝐴 ∈ On ↔ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ∈
On)) |
| 57 | | eleq2 2830 |
. . . . . . . . . 10
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (∅ ∈
𝐴 ↔ ∅ ∈
if((𝐴 ∈ On ∧
∅ ∈ 𝐴), 𝐴,
1o))) |
| 58 | 56, 57 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝐴 = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → ((𝐴 ∈ On ∧ ∅ ∈ 𝐴) ↔ (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ∈ On ∧ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1o)))) |
| 59 | | eleq1 2829 |
. . . . . . . . . 10
⊢
(1o = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (1o
∈ On ↔ if((𝐴
∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ∈
On)) |
| 60 | | eleq2 2830 |
. . . . . . . . . 10
⊢
(1o = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → (∅ ∈
1o ↔ ∅ ∈ if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o))) |
| 61 | 59, 60 | anbi12d 632 |
. . . . . . . . 9
⊢
(1o = if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) → ((1o
∈ On ∧ ∅ ∈ 1o) ↔ (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ∈ On ∧ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1o)))) |
| 62 | | 1on 8518 |
. . . . . . . . . 10
⊢
1o ∈ On |
| 63 | | 0lt1o 8542 |
. . . . . . . . . 10
⊢ ∅
∈ 1o |
| 64 | 62, 63 | pm3.2i 470 |
. . . . . . . . 9
⊢
(1o ∈ On ∧ ∅ ∈
1o) |
| 65 | 58, 61, 64 | elimhyp 4591 |
. . . . . . . 8
⊢
(if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴, 1o) ∈ On
∧ ∅ ∈ if((𝐴
∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o)) |
| 66 | 65 | simpli 483 |
. . . . . . 7
⊢ if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1o) ∈ On |
| 67 | 65 | simpri 485 |
. . . . . . 7
⊢ ∅
∈ if((𝐴 ∈ On
∧ ∅ ∈ 𝐴),
𝐴,
1o) |
| 68 | 66, 67 | oeoelem 8636 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((if((𝐴 ∈ On ∧ ∅ ∈
𝐴), 𝐴, 1o) ↑o 𝐵) ↑o 𝐶) = (if((𝐴 ∈ On ∧ ∅ ∈ 𝐴), 𝐴, 1o) ↑o (𝐵 ·o 𝐶))) |
| 69 | 55, 68 | dedth 4584 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ∅ ∈
𝐴) → ((𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶)))) |
| 70 | 69 | imp 406 |
. . . 4
⊢ (((𝐴 ∈ On ∧ ∅ ∈
𝐴) ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶))) |
| 71 | 70 | an32s 652 |
. . 3
⊢ (((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) ∧ ∅
∈ 𝐴) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶))) |
| 72 | 50, 71 | oe0lem 8551 |
. 2
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝐶 ∈ On)) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶))) |
| 73 | 72 | 3impb 1115 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑o 𝐵) ↑o 𝐶) = (𝐴 ↑o (𝐵 ·o 𝐶))) |