Proof of Theorem oesuclem
Step | Hyp | Ref
| Expression |
1 | | oveq1 7229 |
. . . 4
⊢ (𝐴 = ∅ → (𝐴 ↑o suc 𝐵) = (∅ ↑o
suc 𝐵)) |
2 | | oesuclem.1 |
. . . . . . . 8
⊢ Lim 𝑋 |
3 | | limord 6281 |
. . . . . . . 8
⊢ (Lim
𝑋 → Ord 𝑋) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢ Ord 𝑋 |
5 | | ordelord 6244 |
. . . . . . 7
⊢ ((Ord
𝑋 ∧ 𝐵 ∈ 𝑋) → Ord 𝐵) |
6 | 4, 5 | mpan 690 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 → Ord 𝐵) |
7 | | 0elsuc 7623 |
. . . . . 6
⊢ (Ord
𝐵 → ∅ ∈ suc
𝐵) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → ∅ ∈ suc 𝐵) |
9 | | limsuc 7637 |
. . . . . . 7
⊢ (Lim
𝑋 → (𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋)) |
10 | 2, 9 | ax-mp 5 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋) |
11 | | ordelon 6246 |
. . . . . . . 8
⊢ ((Ord
𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ∈ On) |
12 | 4, 11 | mpan 690 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ∈ On) |
13 | | oe0m1 8257 |
. . . . . . 7
⊢ (suc
𝐵 ∈ On → (∅
∈ suc 𝐵 ↔
(∅ ↑o suc 𝐵) = ∅)) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → (∅ ∈ suc 𝐵 ↔ (∅
↑o suc 𝐵) =
∅)) |
15 | 10, 14 | sylbi 220 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → (∅ ∈ suc 𝐵 ↔ (∅
↑o suc 𝐵) =
∅)) |
16 | 8, 15 | mpbid 235 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → (∅ ↑o suc
𝐵) =
∅) |
17 | 1, 16 | sylan9eqr 2801 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → (𝐴 ↑o suc 𝐵) = ∅) |
18 | | oveq1 7229 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑o 𝐵) = (∅ ↑o
𝐵)) |
19 | | id 22 |
. . . . 5
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
20 | 18, 19 | oveq12d 7240 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑o 𝐵) ·o 𝐴) = ((∅ ↑o
𝐵) ·o
∅)) |
21 | | ordelon 6246 |
. . . . . . 7
⊢ ((Ord
𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ On) |
22 | 4, 21 | mpan 690 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ On) |
23 | | oveq2 7230 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → (∅
↑o 𝐵) =
(∅ ↑o ∅)) |
24 | | oe0m0 8256 |
. . . . . . . . . 10
⊢ (∅
↑o ∅) = 1o |
25 | | 1on 8218 |
. . . . . . . . . 10
⊢
1o ∈ On |
26 | 24, 25 | eqeltri 2835 |
. . . . . . . . 9
⊢ (∅
↑o ∅) ∈ On |
27 | 23, 26 | eqeltrdi 2847 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (∅
↑o 𝐵)
∈ On) |
28 | 27 | adantl 485 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐵 = ∅) → (∅
↑o 𝐵)
∈ On) |
29 | | oe0m1 8257 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑o 𝐵) =
∅)) |
30 | 22, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑋 → (∅ ∈ 𝐵 ↔ (∅ ↑o 𝐵) = ∅)) |
31 | 30 | biimpa 480 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) = ∅) |
32 | | 0elon 6275 |
. . . . . . . . 9
⊢ ∅
∈ On |
33 | 31, 32 | eqeltrdi 2847 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On) |
34 | 33 | adantll 714 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐵) → (∅ ↑o 𝐵) ∈ On) |
35 | 28, 34 | oe0lem 8249 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐵 ∈ 𝑋) → (∅ ↑o 𝐵) ∈ On) |
36 | 22, 35 | mpancom 688 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → (∅ ↑o 𝐵) ∈ On) |
37 | | om0 8253 |
. . . . 5
⊢ ((∅
↑o 𝐵)
∈ On → ((∅ ↑o 𝐵) ·o ∅) =
∅) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → ((∅ ↑o 𝐵) ·o ∅)
= ∅) |
39 | 20, 38 | sylan9eqr 2801 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → ((𝐴 ↑o 𝐵) ·o 𝐴) = ∅) |
40 | 17, 39 | eqtr4d 2781 |
. 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 220 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → suc 𝐵 ∈ On) |
44 | | oevn0 8251 |
. . . 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 7255 |
. . . . 5
⊢ (𝐴 ↑o 𝐵) ∈ V |
47 | | oveq1 7229 |
. . . . . 6
⊢ (𝑥 = (𝐴 ↑o 𝐵) → (𝑥 ·o 𝐴) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
48 | | eqid 2738 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)) = (𝑥 ∈ V ↦ (𝑥 ·o 𝐴)) |
49 | | ovex 7255 |
. . . . . 6
⊢ ((𝐴 ↑o 𝐵) ·o 𝐴) ∈ V |
50 | 47, 48, 49 | fvmpt 6827 |
. . . . 5
⊢ ((𝐴 ↑o 𝐵) ∈ V → ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴 ↑o 𝐵)) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
51 | 46, 50 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴 ↑o 𝐵)) = ((𝐴 ↑o 𝐵) ·o 𝐴) |
52 | | oevn0 8251 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) |
53 | 22, 52 | sylanl2 681 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) |
54 | 53 | fveq2d 6730 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(𝐴 ↑o 𝐵)) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) |
55 | 51, 54 | eqtr3id 2793 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → ((𝐴 ↑o 𝐵) ·o 𝐴) = ((𝑥 ∈ V ↦ (𝑥 ·o 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵))) |
56 | 42, 45, 55 | 3eqtr4d 2788 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |
57 | 40, 56 | oe0lem 8249 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) → (𝐴 ↑o suc 𝐵) = ((𝐴 ↑o 𝐵) ·o 𝐴)) |