Proof of Theorem oesuclem
Step | Hyp | Ref
| Expression |
1 | | oveq1 6556 |
. . . 4
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜 suc
𝐵) = (∅
↑𝑜 suc 𝐵)) |
2 | | oesuclem.1 |
. . . . . . . 8
⊢ Lim 𝑋 |
3 | | limord 5701 |
. . . . . . . 8
⊢ (Lim
𝑋 → Ord 𝑋) |
4 | 2, 3 | ax-mp 5 |
. . . . . . 7
⊢ Ord 𝑋 |
5 | | ordelord 5662 |
. . . . . . 7
⊢ ((Ord
𝑋 ∧ 𝐵 ∈ 𝑋) → Ord 𝐵) |
6 | 4, 5 | mpan 702 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 → Ord 𝐵) |
7 | | 0elsuc 6927 |
. . . . . 6
⊢ (Ord
𝐵 → ∅ ∈ suc
𝐵) |
8 | 6, 7 | syl 17 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → ∅ ∈ suc 𝐵) |
9 | | limsuc 6941 |
. . . . . . 7
⊢ (Lim
𝑋 → (𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋)) |
10 | 2, 9 | ax-mp 5 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 ↔ suc 𝐵 ∈ 𝑋) |
11 | | ordelon 5664 |
. . . . . . . 8
⊢ ((Ord
𝑋 ∧ suc 𝐵 ∈ 𝑋) → suc 𝐵 ∈ On) |
12 | 4, 11 | mpan 702 |
. . . . . . 7
⊢ (suc
𝐵 ∈ 𝑋 → suc 𝐵 ∈ On) |
13 | | oe0m1 7488 |
. . . . . . 7
⊢ (suc
𝐵 ∈ On → (∅
∈ suc 𝐵 ↔
(∅ ↑𝑜 suc 𝐵) = ∅)) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (suc
𝐵 ∈ 𝑋 → (∅ ∈ suc 𝐵 ↔ (∅
↑𝑜 suc 𝐵) = ∅)) |
15 | 10, 14 | sylbi 206 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → (∅ ∈ suc 𝐵 ↔ (∅
↑𝑜 suc 𝐵) = ∅)) |
16 | 8, 15 | mpbid 221 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → (∅ ↑𝑜
suc 𝐵) =
∅) |
17 | 1, 16 | sylan9eqr 2666 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 suc 𝐵) = ∅) |
18 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = ∅ → (𝐴 ↑𝑜
𝐵) = (∅
↑𝑜 𝐵)) |
19 | | id 22 |
. . . . 5
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
20 | 18, 19 | oveq12d 6567 |
. . . 4
⊢ (𝐴 = ∅ → ((𝐴 ↑𝑜
𝐵)
·𝑜 𝐴) = ((∅ ↑𝑜
𝐵)
·𝑜 ∅)) |
21 | | ordelon 5664 |
. . . . . . 7
⊢ ((Ord
𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐵 ∈ On) |
22 | 4, 21 | mpan 702 |
. . . . . 6
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ On) |
23 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) = (∅ ↑𝑜
∅)) |
24 | | oe0m0 7487 |
. . . . . . . . . 10
⊢ (∅
↑𝑜 ∅) = 1𝑜 |
25 | | 1on 7454 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
26 | 24, 25 | eqeltri 2684 |
. . . . . . . . 9
⊢ (∅
↑𝑜 ∅) ∈ On |
27 | 23, 26 | syl6eqel 2696 |
. . . . . . . 8
⊢ (𝐵 = ∅ → (∅
↑𝑜 𝐵) ∈ On) |
28 | 27 | adantl 481 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐵 = ∅) → (∅
↑𝑜 𝐵) ∈ On) |
29 | | oe0m1 7488 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ On → (∅
∈ 𝐵 ↔ (∅
↑𝑜 𝐵) = ∅)) |
30 | 22, 29 | syl 17 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑋 → (∅ ∈ 𝐵 ↔ (∅ ↑𝑜
𝐵) =
∅)) |
31 | 30 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜
𝐵) =
∅) |
32 | | 0elon 5695 |
. . . . . . . . 9
⊢ ∅
∈ On |
33 | 31, 32 | syl6eqel 2696 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑋 ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜
𝐵) ∈
On) |
34 | 33 | adantll 746 |
. . . . . . 7
⊢ (((𝐵 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐵) → (∅ ↑𝑜
𝐵) ∈
On) |
35 | 28, 34 | oe0lem 7480 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐵 ∈ 𝑋) → (∅ ↑𝑜
𝐵) ∈
On) |
36 | 22, 35 | mpancom 700 |
. . . . 5
⊢ (𝐵 ∈ 𝑋 → (∅ ↑𝑜
𝐵) ∈
On) |
37 | | om0 7484 |
. . . . 5
⊢ ((∅
↑𝑜 𝐵) ∈ On → ((∅
↑𝑜 𝐵) ·𝑜 ∅) =
∅) |
38 | 36, 37 | syl 17 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → ((∅ ↑𝑜
𝐵)
·𝑜 ∅) = ∅) |
39 | 20, 38 | sylan9eqr 2666 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴) =
∅) |
40 | 17, 39 | eqtr4d 2647 |
. 2
⊢ ((𝐵 ∈ 𝑋 ∧ 𝐴 = ∅) → (𝐴 ↑𝑜 suc 𝐵) = ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴)) |
41 | | oesuclem.2 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵))) |
42 | 41 | ad2antlr 759 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘suc 𝐵) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵))) |
43 | 10, 12 | sylbi 206 |
. . . 4
⊢ (𝐵 ∈ 𝑋 → suc 𝐵 ∈ On) |
44 | | oevn0 7482 |
. . . 4
⊢ (((𝐴 ∈ On ∧ suc 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜 suc
𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘suc 𝐵)) |
45 | 43, 44 | sylanl2 681 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 suc 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘suc 𝐵)) |
46 | | ovex 6577 |
. . . . 5
⊢ (𝐴 ↑𝑜
𝐵) ∈
V |
47 | | oveq1 6556 |
. . . . . 6
⊢ (𝑥 = (𝐴 ↑𝑜 𝐵) → (𝑥 ·𝑜 𝐴) = ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴)) |
48 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)) = (𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)) |
49 | | ovex 6577 |
. . . . . 6
⊢ ((𝐴 ↑𝑜
𝐵)
·𝑜 𝐴) ∈ V |
50 | 47, 48, 49 | fvmpt 6191 |
. . . . 5
⊢ ((𝐴 ↑𝑜
𝐵) ∈ V → ((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴))‘(𝐴 ↑𝑜
𝐵)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴)) |
51 | 46, 50 | ax-mp 5 |
. . . 4
⊢ ((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴))‘(𝐴 ↑𝑜
𝐵)) = ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴) |
52 | | oevn0 7482 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝐴 ↑𝑜
𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵)) |
53 | 22, 52 | sylanl2 681 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴)),
1𝑜)‘𝐵)) |
54 | 53 | fveq2d 6107 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(𝐴 ↑𝑜 𝐵)) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵))) |
55 | 51, 54 | syl5eqr 2658 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴) = ((𝑥 ∈ V ↦ (𝑥 ·𝑜 𝐴))‘(rec((𝑥 ∈ V ↦ (𝑥 ·𝑜
𝐴)),
1𝑜)‘𝐵))) |
56 | 42, 45, 55 | 3eqtr4d 2654 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) ∧ ∅ ∈ 𝐴) → (𝐴 ↑𝑜 suc 𝐵) = ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴)) |
57 | 40, 56 | oe0lem 7480 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝑋) → (𝐴 ↑𝑜 suc 𝐵) = ((𝐴 ↑𝑜 𝐵) ·𝑜
𝐴)) |