Step | Hyp | Ref
| Expression |
1 | | 2onn 7720 |
. . . . . . . 8
⊢
2𝑜 ∈ ω |
2 | | nnon 7071 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω → 𝑁 ∈ On) |
3 | | 2on 7568 |
. . . . . . . . . . . . . 14
⊢
2𝑜 ∈ On |
4 | | oawordeu 7635 |
. . . . . . . . . . . . . 14
⊢
(((2𝑜 ∈ On ∧ 𝑁 ∈ On) ∧ 2𝑜
⊆ 𝑁) →
∃!𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) |
5 | 3, 4 | mpanl1 716 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ On ∧
2𝑜 ⊆ 𝑁) → ∃!𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) |
6 | | riotasbc 6626 |
. . . . . . . . . . . . 13
⊢
(∃!𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁 → [(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) / 𝑜](2𝑜
+𝑜 𝑜) =
𝑁) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ On ∧
2𝑜 ⊆ 𝑁) → [(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) / 𝑜](2𝑜
+𝑜 𝑜) =
𝑁) |
8 | | riotaex 6615 |
. . . . . . . . . . . . . 14
⊢
(℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ V |
9 | | sbceq1g 3988 |
. . . . . . . . . . . . . 14
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ V →
([(℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) / 𝑜](2𝑜
+𝑜 𝑜) =
𝑁 ↔
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌(2𝑜
+𝑜 𝑜) =
𝑁)) |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
([(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜](2𝑜
+𝑜 𝑜) =
𝑁 ↔
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌(2𝑜
+𝑜 𝑜) =
𝑁) |
11 | | csbov2g 6691 |
. . . . . . . . . . . . . . . 16
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ V →
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌(2𝑜
+𝑜 𝑜) =
(2𝑜 +𝑜
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌𝑜)) |
12 | 8, 11 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌(2𝑜
+𝑜 𝑜) =
(2𝑜 +𝑜
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌𝑜) |
13 | | csbvarg 4003 |
. . . . . . . . . . . . . . . . 17
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ V →
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) |
14 | 8, 13 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
⊢
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌𝑜 = (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) |
15 | 14 | oveq2i 6661 |
. . . . . . . . . . . . . . 15
⊢
(2𝑜 +𝑜
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌𝑜) = (2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) |
16 | 12, 15 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢
⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌(2𝑜
+𝑜 𝑜) =
(2𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) |
17 | 16 | eqeq1i 2627 |
. . . . . . . . . . . . 13
⊢
(⦋(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜⦌(2𝑜
+𝑜 𝑜) =
𝑁 ↔
(2𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) = 𝑁) |
18 | 10, 17 | bitri 264 |
. . . . . . . . . . . 12
⊢
([(℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) / 𝑜](2𝑜
+𝑜 𝑜) =
𝑁 ↔
(2𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) = 𝑁) |
19 | 7, 18 | sylib 208 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ On ∧
2𝑜 ⊆ 𝑁) → (2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) = 𝑁) |
20 | 2, 19 | sylan 488 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) = 𝑁) |
21 | | simpl 473 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → 𝑁 ∈ ω) |
22 | 20, 21 | eqeltrd 2701 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ∈
ω) |
23 | | riotacl 6625 |
. . . . . . . . . . 11
⊢
(∃!𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁 → (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
On) |
24 | | riotaund 6647 |
. . . . . . . . . . . 12
⊢ (¬
∃!𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁 → (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) =
∅) |
25 | | 0elon 5778 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
26 | 24, 25 | syl6eqel 2709 |
. . . . . . . . . . 11
⊢ (¬
∃!𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁 → (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
On) |
27 | 23, 26 | pm2.61i 176 |
. . . . . . . . . 10
⊢
(℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ On |
28 | | nnarcl 7696 |
. . . . . . . . . . . 12
⊢
((2𝑜 ∈ On ∧ (℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) ∈ On) → ((2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ∈ ω ↔
(2𝑜 ∈ ω ∧ (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
ω))) |
29 | 3, 28 | mpan 706 |
. . . . . . . . . . 11
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ On → ((2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ∈ ω ↔
(2𝑜 ∈ ω ∧ (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
ω))) |
30 | 1 | biantrur 527 |
. . . . . . . . . . 11
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω ↔
(2𝑜 ∈ ω ∧ (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
ω)) |
31 | 29, 30 | syl6bbr 278 |
. . . . . . . . . 10
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ On → ((2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ∈ ω ↔
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω)) |
32 | 27, 31 | ax-mp 5 |
. . . . . . . . 9
⊢
((2𝑜 +𝑜 (℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁)) ∈ ω ↔
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω) |
33 | 22, 32 | sylib 208 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
ω) |
34 | | nnacom 7697 |
. . . . . . . 8
⊢
((2𝑜 ∈ ω ∧ (℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω) →
(2𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) = ((℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) +𝑜
2𝑜)) |
35 | 1, 33, 34 | sylancr 695 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) = ((℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) +𝑜
2𝑜)) |
36 | | df-2o 7561 |
. . . . . . . . 9
⊢
2𝑜 = suc 1𝑜 |
37 | 36 | oveq2i 6661 |
. . . . . . . 8
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) +𝑜
2𝑜) = ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
suc 1𝑜) |
38 | | 1onn 7719 |
. . . . . . . . 9
⊢
1𝑜 ∈ ω |
39 | | nnasuc 7686 |
. . . . . . . . 9
⊢
(((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω ∧ 1𝑜
∈ ω) → ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
suc 1𝑜) = suc ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
1𝑜)) |
40 | 33, 38, 39 | sylancl 694 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
suc 1𝑜) = suc ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
1𝑜)) |
41 | 37, 40 | syl5eq 2668 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
2𝑜) = suc ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
1𝑜)) |
42 | 35, 20, 41 | 3eqtr3d 2664 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → 𝑁 = suc ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
1𝑜)) |
43 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → 𝑁 ∈ On) |
44 | | sucidg 5803 |
. . . . . . . . . . . 12
⊢
(1𝑜 ∈ ω → 1𝑜
∈ suc 1𝑜) |
45 | 38, 44 | ax-mp 5 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ suc 1𝑜 |
46 | 45, 36 | eleqtrri 2700 |
. . . . . . . . . 10
⊢
1𝑜 ∈ 2𝑜 |
47 | | ssel 3597 |
. . . . . . . . . 10
⊢
(2𝑜 ⊆ 𝑁 → (1𝑜 ∈
2𝑜 → 1𝑜 ∈ 𝑁)) |
48 | 46, 47 | mpi 20 |
. . . . . . . . 9
⊢
(2𝑜 ⊆ 𝑁 → 1𝑜 ∈ 𝑁) |
49 | | ne0i 3921 |
. . . . . . . . 9
⊢
(1𝑜 ∈ 𝑁 → 𝑁 ≠ ∅) |
50 | 48, 49 | syl 17 |
. . . . . . . 8
⊢
(2𝑜 ⊆ 𝑁 → 𝑁 ≠ ∅) |
51 | 50 | adantl 482 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → 𝑁 ≠ ∅) |
52 | | nnlim 7078 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → ¬ Lim
𝑁) |
53 | 52 | adantr 481 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → ¬ Lim 𝑁) |
54 | | onsucuni3 33215 |
. . . . . . 7
⊢ ((𝑁 ∈ On ∧ 𝑁 ≠ ∅ ∧ ¬ Lim
𝑁) → 𝑁 = suc ∪ 𝑁) |
55 | 43, 51, 53, 54 | syl3anc 1326 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → 𝑁 = suc ∪ 𝑁) |
56 | | nnacom 7697 |
. . . . . . . 8
⊢
(((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω ∧ 1𝑜
∈ ω) → ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
1𝑜) = (1𝑜 +𝑜
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁))) |
57 | 33, 38, 56 | sylancl 694 |
. . . . . . 7
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → ((℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) +𝑜
1𝑜) = (1𝑜 +𝑜
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁))) |
58 | | suceq 5790 |
. . . . . . 7
⊢
(((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) +𝑜
1𝑜) = (1𝑜 +𝑜
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁)) → suc ((℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) +𝑜
1𝑜) = suc (1𝑜 +𝑜
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁))) |
59 | 57, 58 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → suc ((℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) +𝑜
1𝑜) = suc (1𝑜 +𝑜
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁))) |
60 | 42, 55, 59 | 3eqtr3d 2664 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → suc ∪
𝑁 = suc
(1𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) |
61 | | ordom 7074 |
. . . . . . . . 9
⊢ Ord
ω |
62 | | ordelss 5739 |
. . . . . . . . 9
⊢ ((Ord
ω ∧ 𝑁 ∈
ω) → 𝑁 ⊆
ω) |
63 | 61, 62 | mpan 706 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → 𝑁 ⊆
ω) |
64 | | nnfi 8153 |
. . . . . . . 8
⊢ (𝑁 ∈ ω → 𝑁 ∈ Fin) |
65 | | nnunifi 8211 |
. . . . . . . 8
⊢ ((𝑁 ⊆ ω ∧ 𝑁 ∈ Fin) → ∪ 𝑁
∈ ω) |
66 | 63, 64, 65 | syl2anc 693 |
. . . . . . 7
⊢ (𝑁 ∈ ω → ∪ 𝑁
∈ ω) |
67 | 66 | adantr 481 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → ∪ 𝑁 ∈
ω) |
68 | | nnacl 7691 |
. . . . . . 7
⊢
((1𝑜 ∈ ω ∧ (℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω) →
(1𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ∈
ω) |
69 | 38, 33, 68 | sylancr 695 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ∈
ω) |
70 | | peano4 7088 |
. . . . . 6
⊢ ((∪ 𝑁
∈ ω ∧ (1𝑜 +𝑜
(℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁)) ∈ ω) → (suc ∪ 𝑁 =
suc (1𝑜 +𝑜 (℩𝑜 ∈ On
(2𝑜 +𝑜 𝑜) = 𝑁)) ↔ ∪ 𝑁 = (1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)))) |
71 | 67, 69, 70 | syl2anc 693 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (suc ∪
𝑁 = suc
(1𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)) ↔ ∪ 𝑁 =
(1𝑜 +𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)))) |
72 | 60, 71 | mpbid 222 |
. . . 4
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → ∪ 𝑁 = (1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) |
73 | 72 | fveq2d 6195 |
. . 3
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (rec(𝐹, 〈∪ 𝑁, (1st ‘𝑦)〉)‘∪ 𝑁) =
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘(1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)))) |
74 | 73 | adantr 481 |
. 2
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈∪ 𝑁, (1st ‘𝑦)〉)‘∪ 𝑁) =
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘(1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)))) |
75 | 33 | adantr 481 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁) ∈
ω) |
76 | | finxpreclem4.1 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
77 | 76 | finxpreclem3 33230 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 〈∪
𝑁, (1st
‘𝑦)〉 = (𝐹‘〈𝑁, 𝑦〉)) |
78 | | df-1o 7560 |
. . . . . . . 8
⊢
1𝑜 = suc ∅ |
79 | 78 | fveq2i 6194 |
. . . . . . 7
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜) =
(rec(𝐹, 〈𝑁, 𝑦〉)‘suc ∅) |
80 | | rdgsuc 7520 |
. . . . . . . 8
⊢ (∅
∈ On → (rec(𝐹,
〈𝑁, 𝑦〉)‘suc ∅) = (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘∅))) |
81 | 25, 80 | ax-mp 5 |
. . . . . . 7
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘suc ∅) = (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘∅)) |
82 | | opex 4932 |
. . . . . . . . 9
⊢
〈𝑁, 𝑦〉 ∈ V |
83 | 82 | rdg0 7517 |
. . . . . . . 8
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘∅) = 〈𝑁, 𝑦〉 |
84 | 83 | fveq2i 6194 |
. . . . . . 7
⊢ (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘∅)) = (𝐹‘〈𝑁, 𝑦〉) |
85 | 79, 81, 84 | 3eqtri 2648 |
. . . . . 6
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜) = (𝐹‘〈𝑁, 𝑦〉) |
86 | 77, 85 | syl6reqr 2675 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜) =
〈∪ 𝑁, (1st ‘𝑦)〉) |
87 | 86 | fveq2d 6195 |
. . . 4
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜)) =
(𝐹‘〈∪ 𝑁,
(1st ‘𝑦)〉)) |
88 | | 2on0 7569 |
. . . . . 6
⊢
2𝑜 ≠ ∅ |
89 | | nnlim 7078 |
. . . . . . 7
⊢
(2𝑜 ∈ ω → ¬ Lim
2𝑜) |
90 | 1, 89 | ax-mp 5 |
. . . . . 6
⊢ ¬
Lim 2𝑜 |
91 | | rdgsucuni 33217 |
. . . . . 6
⊢
((2𝑜 ∈ On ∧ 2𝑜 ≠
∅ ∧ ¬ Lim 2𝑜) → (rec(𝐹, 〈𝑁, 𝑦〉)‘2𝑜) = (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘∪
2𝑜))) |
92 | 3, 88, 90, 91 | mp3an 1424 |
. . . . 5
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘2𝑜) = (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘∪
2𝑜)) |
93 | | 1oequni2o 33216 |
. . . . . . 7
⊢
1𝑜 = ∪
2𝑜 |
94 | 93 | fveq2i 6194 |
. . . . . 6
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜) =
(rec(𝐹, 〈𝑁, 𝑦〉)‘∪
2𝑜) |
95 | 94 | fveq2i 6194 |
. . . . 5
⊢ (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜)) =
(𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘∪
2𝑜)) |
96 | 92, 95 | eqtr4i 2647 |
. . . 4
⊢
(rec(𝐹, 〈𝑁, 𝑦〉)‘2𝑜) = (𝐹‘(rec(𝐹, 〈𝑁, 𝑦〉)‘1𝑜)) |
97 | 78 | fveq2i 6194 |
. . . . 5
⊢
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘1𝑜) =
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘suc ∅) |
98 | | rdgsuc 7520 |
. . . . . 6
⊢ (∅
∈ On → (rec(𝐹,
〈∪ 𝑁, (1st ‘𝑦)〉)‘suc ∅) = (𝐹‘(rec(𝐹, 〈∪ 𝑁, (1st ‘𝑦)〉)‘∅))) |
99 | 25, 98 | ax-mp 5 |
. . . . 5
⊢
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘suc ∅) = (𝐹‘(rec(𝐹, 〈∪ 𝑁, (1st ‘𝑦)〉)‘∅)) |
100 | | opex 4932 |
. . . . . . 7
⊢
〈∪ 𝑁, (1st ‘𝑦)〉 ∈ V |
101 | 100 | rdg0 7517 |
. . . . . 6
⊢
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘∅) = 〈∪ 𝑁,
(1st ‘𝑦)〉 |
102 | 101 | fveq2i 6194 |
. . . . 5
⊢ (𝐹‘(rec(𝐹, 〈∪ 𝑁, (1st ‘𝑦)〉)‘∅)) =
(𝐹‘〈∪ 𝑁,
(1st ‘𝑦)〉) |
103 | 97, 99, 102 | 3eqtri 2648 |
. . . 4
⊢
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘1𝑜) =
(𝐹‘〈∪ 𝑁,
(1st ‘𝑦)〉) |
104 | 87, 96, 103 | 3eqtr4g 2681 |
. . 3
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑁, 𝑦〉)‘2𝑜) =
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘1𝑜)) |
105 | | 1on 7567 |
. . . 4
⊢
1𝑜 ∈ On |
106 | | rdgeqoa 33218 |
. . . 4
⊢
((2𝑜 ∈ On ∧ 1𝑜 ∈ On
∧ (℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω) → ((rec(𝐹, 〈𝑁, 𝑦〉)‘2𝑜) =
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘1𝑜) →
(rec(𝐹, 〈𝑁, 𝑦〉)‘(2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) = (rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘(1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))))) |
107 | 3, 105, 106 | mp3an12 1414 |
. . 3
⊢
((℩𝑜
∈ On (2𝑜 +𝑜 𝑜) = 𝑁) ∈ ω → ((rec(𝐹, 〈𝑁, 𝑦〉)‘2𝑜) =
(rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘1𝑜) →
(rec(𝐹, 〈𝑁, 𝑦〉)‘(2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) = (rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘(1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))))) |
108 | 75, 104, 107 | sylc 65 |
. 2
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑁, 𝑦〉)‘(2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) = (rec(𝐹, 〈∪ 𝑁,
(1st ‘𝑦)〉)‘(1𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁)))) |
109 | 20 | fveq2d 6195 |
. . 3
⊢ ((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) → (rec(𝐹, 〈𝑁, 𝑦〉)‘(2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁)) |
110 | 109 | adantr 481 |
. 2
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑁, 𝑦〉)‘(2𝑜
+𝑜 (℩𝑜 ∈ On (2𝑜
+𝑜 𝑜) =
𝑁))) = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁)) |
111 | 74, 108, 110 | 3eqtr2rd 2663 |
1
⊢ (((𝑁 ∈ ω ∧
2𝑜 ⊆ 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁) = (rec(𝐹, 〈∪ 𝑁, (1st ‘𝑦)〉)‘∪ 𝑁)) |