Step | Hyp | Ref
| Expression |
1 | | peano2 7668 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ω → suc 𝑁 ∈
ω) |
2 | 1 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ suc 𝑁 ∈
ω) |
3 | | 1on 8209 |
. . . . . . . . . . . . 13
⊢
1o ∈ On |
4 | 3 | onordi 6318 |
. . . . . . . . . . . 12
⊢ Ord
1o |
5 | | nnord 7652 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ω → Ord 𝑁) |
6 | | ordsseleq 6242 |
. . . . . . . . . . . 12
⊢ ((Ord
1o ∧ Ord 𝑁)
→ (1o ⊆ 𝑁 ↔ (1o ∈ 𝑁 ∨ 1o = 𝑁))) |
7 | 4, 5, 6 | sylancr 590 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω →
(1o ⊆ 𝑁
↔ (1o ∈ 𝑁 ∨ 1o = 𝑁))) |
8 | 7 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (1o ∈ 𝑁 ∨ 1o = 𝑁)) |
9 | | elelsuc 6285 |
. . . . . . . . . . . . 13
⊢
(1o ∈ 𝑁 → 1o ∈ suc 𝑁) |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ω →
(1o ∈ 𝑁
→ 1o ∈ suc 𝑁)) |
11 | | sucidg 6291 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ω → 𝑁 ∈ suc 𝑁) |
12 | | eleq1 2825 |
. . . . . . . . . . . . 13
⊢
(1o = 𝑁
→ (1o ∈ suc 𝑁 ↔ 𝑁 ∈ suc 𝑁)) |
13 | 11, 12 | syl5ibrcom 250 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ω →
(1o = 𝑁 →
1o ∈ suc 𝑁)) |
14 | 10, 13 | jaod 859 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω →
((1o ∈ 𝑁
∨ 1o = 𝑁)
→ 1o ∈ suc 𝑁)) |
15 | 14 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ ((1o ∈ 𝑁 ∨ 1o = 𝑁) → 1o ∈ suc 𝑁)) |
16 | 8, 15 | mpd 15 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ 1o ∈ suc 𝑁) |
17 | | finxpsuclem.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
18 | 17 | finxpreclem6 35304 |
. . . . . . . . 9
⊢ ((suc
𝑁 ∈ ω ∧
1o ∈ suc 𝑁)
→ (𝑈↑↑suc
𝑁) ⊆ (V × 𝑈)) |
19 | 2, 16, 18 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑈↑↑suc
𝑁) ⊆ (V × 𝑈)) |
20 | 19 | sselda 3901 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → 𝑦 ∈ (V × 𝑈)) |
21 | 1 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → suc 𝑁 ∈
ω) |
22 | | df-2o 8203 |
. . . . . . . . . . . . . . 15
⊢
2o = suc 1o |
23 | | ordsucsssuc 7602 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
1o ∧ Ord 𝑁)
→ (1o ⊆ 𝑁 ↔ suc 1o ⊆ suc 𝑁)) |
24 | 4, 5, 23 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ω →
(1o ⊆ 𝑁
↔ suc 1o ⊆ suc 𝑁)) |
25 | 24 | biimpa 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ suc 1o ⊆ suc 𝑁) |
26 | 22, 25 | eqsstrid 3949 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ 2o ⊆ suc 𝑁) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → 2o
⊆ suc 𝑁) |
28 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → 𝑦 ∈ (V × 𝑈)) |
29 | 17 | finxpreclem4 35302 |
. . . . . . . . . . . . 13
⊢ (((suc
𝑁 ∈ ω ∧
2o ⊆ suc 𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁) = (rec(𝐹, 〈∪ suc
𝑁, (1st
‘𝑦)〉)‘∪
suc 𝑁)) |
30 | 21, 27, 28, 29 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁) = (rec(𝐹, 〈∪ suc
𝑁, (1st
‘𝑦)〉)‘∪
suc 𝑁)) |
31 | | ordunisuc 7611 |
. . . . . . . . . . . . . . . 16
⊢ (Ord
𝑁 → ∪ suc 𝑁 = 𝑁) |
32 | 5, 31 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ω → ∪ suc 𝑁 = 𝑁) |
33 | | opeq1 4784 |
. . . . . . . . . . . . . . . 16
⊢ (∪ suc 𝑁 = 𝑁 → 〈∪
suc 𝑁, (1st
‘𝑦)〉 =
〈𝑁, (1st
‘𝑦)〉) |
34 | | rdgeq2 8148 |
. . . . . . . . . . . . . . . 16
⊢
(〈∪ suc 𝑁, (1st ‘𝑦)〉 = 〈𝑁, (1st ‘𝑦)〉 → rec(𝐹, 〈∪ suc
𝑁, (1st
‘𝑦)〉) =
rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (∪ suc 𝑁 = 𝑁 → rec(𝐹, 〈∪ suc
𝑁, (1st
‘𝑦)〉) =
rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)) |
36 | 32, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ω → rec(𝐹, 〈∪ suc 𝑁, (1st ‘𝑦)〉) = rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)) |
37 | 36, 32 | fveq12d 6724 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ω →
(rec(𝐹, 〈∪ suc 𝑁, (1st ‘𝑦)〉)‘∪
suc 𝑁) = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁)) |
38 | 37 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (rec(𝐹, 〈∪ suc 𝑁, (1st ‘𝑦)〉)‘∪
suc 𝑁) = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁)) |
39 | 30, 38 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁) = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁)) |
40 | 39 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (∅ =
(rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁) ↔ ∅ = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁))) |
41 | 17 | dffinxpf 35293 |
. . . . . . . . . . . . 13
⊢ (𝑈↑↑suc 𝑁) = {𝑦 ∣ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁))} |
42 | 41 | abeq2i 2872 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁))) |
43 | 1 | biantrurd 536 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ω → (∅
= (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁) ↔ (suc 𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁)))) |
44 | 42, 43 | bitr4id 293 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ∅ = (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁))) |
45 | 44 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ∅ = (rec(𝐹, 〈suc 𝑁, 𝑦〉)‘suc 𝑁))) |
46 | | fvex 6730 |
. . . . . . . . . . . . 13
⊢
(1st ‘𝑦) ∈ V |
47 | | opeq2 4785 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (1st ‘𝑦) → 〈𝑁, 𝑧〉 = 〈𝑁, (1st ‘𝑦)〉) |
48 | | rdgeq2 8148 |
. . . . . . . . . . . . . . . . 17
⊢
(〈𝑁, 𝑧〉 = 〈𝑁, (1st ‘𝑦)〉 → rec(𝐹, 〈𝑁, 𝑧〉) = rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (1st ‘𝑦) → rec(𝐹, 〈𝑁, 𝑧〉) = rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)) |
50 | 49 | fveq1d 6719 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (1st ‘𝑦) → (rec(𝐹, 〈𝑁, 𝑧〉)‘𝑁) = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁)) |
51 | 50 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (1st ‘𝑦) → (∅ = (rec(𝐹, 〈𝑁, 𝑧〉)‘𝑁) ↔ ∅ = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁))) |
52 | 51 | anbi2d 632 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (1st ‘𝑦) → ((𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, 𝑧〉)‘𝑁)) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁)))) |
53 | 17 | dffinxpf 35293 |
. . . . . . . . . . . . 13
⊢ (𝑈↑↑𝑁) = {𝑧 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, 𝑧〉)‘𝑁))} |
54 | 46, 52, 53 | elab2 3591 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑦) ∈ (𝑈↑↑𝑁) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁))) |
55 | 54 | baib 539 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ω →
((1st ‘𝑦)
∈ (𝑈↑↑𝑁) ↔ ∅ = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁))) |
56 | 55 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → ((1st
‘𝑦) ∈ (𝑈↑↑𝑁) ↔ ∅ = (rec(𝐹, 〈𝑁, (1st ‘𝑦)〉)‘𝑁))) |
57 | 40, 45, 56 | 3bitr4d 314 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ (1st ‘𝑦) ∈ (𝑈↑↑𝑁))) |
58 | 57 | biimpd 232 |
. . . . . . . 8
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (V ×
𝑈)) → (𝑦 ∈ (𝑈↑↑suc 𝑁) → (1st ‘𝑦) ∈ (𝑈↑↑𝑁))) |
59 | 58 | impancom 455 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → (𝑦 ∈ (V × 𝑈) → (1st ‘𝑦) ∈ (𝑈↑↑𝑁))) |
60 | 20, 59 | mpd 15 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
∧ 𝑦 ∈ (𝑈↑↑suc 𝑁)) → (1st
‘𝑦) ∈ (𝑈↑↑𝑁)) |
61 | 60 | ex 416 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑦 ∈ (𝑈↑↑suc 𝑁) → (1st
‘𝑦) ∈ (𝑈↑↑𝑁))) |
62 | 20 | ex 416 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑦 ∈ (𝑈↑↑suc 𝑁) → 𝑦 ∈ (V × 𝑈))) |
63 | 61, 62 | jcad 516 |
. . . 4
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑦 ∈ (𝑈↑↑suc 𝑁) → ((1st
‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)))) |
64 | 57 | exbiri 811 |
. . . . . 6
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑦 ∈ (V ×
𝑈) → ((1st
‘𝑦) ∈ (𝑈↑↑𝑁) → 𝑦 ∈ (𝑈↑↑suc 𝑁)))) |
65 | 64 | impd 414 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ ((𝑦 ∈ (V
× 𝑈) ∧
(1st ‘𝑦)
∈ (𝑈↑↑𝑁)) → 𝑦 ∈ (𝑈↑↑suc 𝑁))) |
66 | 65 | ancomsd 469 |
. . . 4
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (((1st ‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)) → 𝑦 ∈ (𝑈↑↑suc 𝑁))) |
67 | 63, 66 | impbid 215 |
. . 3
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ ((1st
‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈)))) |
68 | | elxp8 35279 |
. . 3
⊢ (𝑦 ∈ ((𝑈↑↑𝑁) × 𝑈) ↔ ((1st ‘𝑦) ∈ (𝑈↑↑𝑁) ∧ 𝑦 ∈ (V × 𝑈))) |
69 | 67, 68 | bitr4di 292 |
. 2
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑦 ∈ (𝑈↑↑suc 𝑁) ↔ 𝑦 ∈ ((𝑈↑↑𝑁) × 𝑈))) |
70 | 69 | eqrdv 2735 |
1
⊢ ((𝑁 ∈ ω ∧
1o ⊆ 𝑁)
→ (𝑈↑↑suc
𝑁) = ((𝑈↑↑𝑁) × 𝑈)) |