Proof of Theorem oesuclem
| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . 4
⊢ (𝐴 = ∅ → (𝐴 ↑o suc 𝐵) = (∅ ↑o
suc 𝐵)) |
| 2 | | oesuclem.1 |
. . . . . . . 8
⊢ Lim 𝑋 |
| 3 | | limord 6444 |
. . . . . . . 8
⊢ (Lim
𝑋 → Ord 𝑋) |
| 4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢ Ord 𝑋 |
| 5 | | ordelord 6406 |
. . . . . . 7
⊢ ((Ord
𝑋 ∧ 𝐵 ∈ 𝑋) → Ord 𝐵) |
| 6 | 4, 5 | mpan 690 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 → Ord 𝐵) |
| 7 | | 0elsuc 7855 |
. . . . . 6
⊢ (Ord
𝐵 → ∅ ∈ suc
𝐵) |
| 8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → ∅ ∈ suc 𝐵) |
| 9 | | limsuc 7870 |
. . . . . . 7
⊢ (Lim
𝑋 → (𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋)) |
| 10 | 2, 9 | ax-mp 5 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋) |
| 11 | | ordelon 6408 |
. . . . . . . 8
⊢ ((Ord
𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ∈ On) |
| 12 | 4, 11 | mpan 690 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ∈ On) |
| 13 | | oe0m1 8559 |
. . . . . . 7
⊢ (suc
𝐵 ∈ On → (∅
∈ suc 𝐵 ↔
(∅ ↑o suc 𝐵) = ∅)) |
| 14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → (∅ ∈ suc 𝐵 ↔ (∅
↑o suc 𝐵) =
∅)) |
| 15 | 10, 14 | sylbi 217 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → (∅ ∈ suc 𝐵 ↔ (∅
↑o suc 𝐵) =
∅)) |
| 16 | 8, 15 | mpbid 232 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → (∅ ↑o suc
𝐵) =
∅) |
| 17 | 1, 16 | sylan9eqr 2799 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → (𝐴 ↑o suc 𝐵) = ∅) |
| 18 | | oveq1 7438 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
| 19 | | id 22 |
. . . . 5
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
| 20 | 18, 19 | oveq12d 7449 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝐵) ·o 𝐴) = ((∅ ↑o
𝐵) ·o
∅)) |
| 21 | | ordelon 6408 |
. . . . . . 7
⊢ ((Ord
𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ On) |
| 22 | 4, 21 | mpan 690 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ On) |
| 23 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → (∅
↑o 𝐵) =
(∅ ↑o ∅)) |
| 24 | | oe0m0 8558 |
. . . . . . . . . 10
⊢ (∅
↑o ∅) = 1o |
| 25 | | 1on 8518 |
. . . . . . . . . 10
⊢
1o ∈ On |
| 26 | 24, 25 | eqeltri 2837 |
. . . . . . . . 9
⊢ (∅
↑o ∅) ∈ On |
| 27 | 23, 26 | eqeltrdi 2849 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (∅
↑o 𝐵)
∈ On) |
| 28 | 27 | adantl 481 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐵 = ∅) → (∅
↑o 𝐵)
∈ On) |
| 29 | | oe0m1 8559 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
| 30 | 22, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑋 → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅)) |
| 31 | 30 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) = ∅) |
| 32 | | 0elon 6438 |
. . . . . . . . 9
⊢ ∅
∈ On |
| 33 | 31, 32 | eqeltrdi 2849 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On) |
| 34 | 33 | adantll 714 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On) |
| 35 | 28, 34 | oe0lem 8551 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐵 ∈ 𝑋) → (∅ ↑o 𝐵) ∈ On) |
| 36 | 22, 35 | mpancom 688 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → (∅ ↑o 𝐵) ∈ On) |
| 37 | | om0 8555 |
. . . . 5
⊢ ((∅
↑o 𝐵)
∈ On → ((∅ ↑o 𝐵) ·o ∅) =
∅) |
| 38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → ((∅ ↑o 𝐵) ·o ∅)
= ∅) |
| 39 | 20, 38 | sylan9eqr 2799 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → ((𝐴 ↑o 𝐵) ·o 𝐴) = ∅) |
| 40 | 17, 39 | eqtr4d 2780 |
. 2
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
| 41 | | oesuclem.2 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) |
| 42 | 41 | ad2antlr 727 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) |
| 43 | 10, 12 | sylbi 217 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → suc 𝐵 ∈ On) |
| 44 | | oevn0 8553 |
. . . 4
⊢ (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑o suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵)) |
| 45 | 43, 44 | sylanl2 681 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘suc 𝐵)) |
| 46 | | ovex 7464 |
. . . . 5
⊢ (𝐴 ↑o 𝐵) ∈ V |
| 47 | | oveq1 7438 |
. . . . . 6
⊢ (𝑥 = (𝐴 ↑o 𝐵) → (𝑥 ·o 𝐴) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
| 48 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)) = (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)) |
| 49 | | ovex 7464 |
. . . . . 6
⊢ ((𝐴 ↑o 𝐵) ·o 𝐴) ∈ V |
| 50 | 47, 48, 49 | fvmpt 7016 |
. . . . 5
⊢ ((𝐴 ↑o 𝐵) ∈ V → ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴 ↑o 𝐵)) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
| 51 | 46, 50 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴 ↑o 𝐵)) = ((𝐴 ↑o 𝐵) ·o 𝐴) |
| 52 | | oevn0 8553 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) |
| 53 | 22, 52 | sylanl2 681 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) |
| 54 | 53 | fveq2d 6910 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴 ↑o 𝐵)) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) |
| 55 | 51, 54 | eqtr3id 2791 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → ((𝐴 ↑o 𝐵) ·o 𝐴) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) |
| 56 | 42, 45, 55 | 3eqtr4d 2787 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
| 57 | 40, 56 | oe0lem 8551 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |