Step | Hyp | Ref
| Expression |
1 | | 1onn 7606 |
. . . . . 6
⊢
1𝑜 ∈ ω |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝑦 ∈ 𝑈 → 1𝑜 ∈
ω) |
3 | | finxpreclem1 32402 |
. . . . . 6
⊢ (𝑦 ∈ 𝑈 → ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉)) |
4 | | 1on 7454 |
. . . . . . . 8
⊢
1𝑜 ∈ On |
5 | | 1n0 7462 |
. . . . . . . 8
⊢
1𝑜 ≠ ∅ |
6 | | nnlim 6970 |
. . . . . . . . 9
⊢
(1𝑜 ∈ ω → ¬ Lim
1𝑜) |
7 | 1, 6 | ax-mp 5 |
. . . . . . . 8
⊢ ¬
Lim 1𝑜 |
8 | | rdgsucuni 32393 |
. . . . . . . 8
⊢
((1𝑜 ∈ On ∧ 1𝑜 ≠
∅ ∧ ¬ Lim 1𝑜) → (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜) =
((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘(rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∪ 1𝑜))) |
9 | 4, 5, 7, 8 | mp3an 1416 |
. . . . . . 7
⊢
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜) =
((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘(rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∪ 1𝑜)) |
10 | | df-1o 7447 |
. . . . . . . . . . . 12
⊢
1𝑜 = suc ∅ |
11 | 10 | unieqi 4381 |
. . . . . . . . . . 11
⊢ ∪ 1𝑜 = ∪ suc
∅ |
12 | | 0elon 5695 |
. . . . . . . . . . . 12
⊢ ∅
∈ On |
13 | 12 | onunisuci 5758 |
. . . . . . . . . . 11
⊢ ∪ suc ∅ = ∅ |
14 | 11, 13 | eqtri 2632 |
. . . . . . . . . 10
⊢ ∪ 1𝑜 = ∅ |
15 | 14 | fveq2i 6106 |
. . . . . . . . 9
⊢
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∪ 1𝑜) = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∅) |
16 | | opex 4859 |
. . . . . . . . . 10
⊢
〈1𝑜, 𝑦〉 ∈ V |
17 | 16 | rdg0 7404 |
. . . . . . . . 9
⊢
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∅) =
〈1𝑜, 𝑦〉 |
18 | 15, 17 | eqtri 2632 |
. . . . . . . 8
⊢
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∪ 1𝑜) = 〈1𝑜,
𝑦〉 |
19 | 18 | fveq2i 6106 |
. . . . . . 7
⊢ ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘(rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘∪ 1𝑜)) = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉) |
20 | 9, 19 | eqtri 2632 |
. . . . . 6
⊢
(rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜) =
((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉) |
21 | 3, 20 | syl6eqr 2662 |
. . . . 5
⊢ (𝑦 ∈ 𝑈 → ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜)) |
22 | | df-finxp 32397 |
. . . . . 6
⊢ (𝑈↑↑1𝑜) = {𝑦 ∣ (1𝑜
∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜))} |
23 | 22 | abeq2i 2722 |
. . . . 5
⊢ (𝑦 ∈ (𝑈↑↑1𝑜) ↔
(1𝑜 ∈ ω ∧ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜))) |
24 | 2, 21, 23 | sylanbrc 695 |
. . . 4
⊢ (𝑦 ∈ 𝑈 → 𝑦 ∈ (𝑈↑↑1𝑜)) |
25 | 1, 23 | mpbiran 955 |
. . . . 5
⊢ (𝑦 ∈ (𝑈↑↑1𝑜) ↔
∅ = (rec((𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜)) |
26 | | vex 3176 |
. . . . . . 7
⊢ 𝑦 ∈ V |
27 | 20 | eqcomi 2619 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉) = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜) |
28 | | finxpreclem2 32403 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈) → ¬ ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉)) |
29 | 28 | neqned 2789 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈) → ∅ ≠ ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉)) |
30 | 29 | necomd 2837 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑦〉) ≠
∅) |
31 | 27, 30 | syl5eqner 2857 |
. . . . . . . . 9
⊢ ((𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈) → (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜) ≠
∅) |
32 | 31 | necomd 2837 |
. . . . . . . 8
⊢ ((𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈) → ∅ ≠ (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜)) |
33 | 32 | neneqd 2787 |
. . . . . . 7
⊢ ((𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝑈) → ¬ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜)) |
34 | 26, 33 | mpan 702 |
. . . . . 6
⊢ (¬
𝑦 ∈ 𝑈 → ¬ ∅ = (rec((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜)) |
35 | 34 | con4i 112 |
. . . . 5
⊢ (∅
= (rec((𝑛 ∈ ω,
𝑥 ∈ V ↦
if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))), 〈1𝑜, 𝑦〉)‘1𝑜) →
𝑦 ∈ 𝑈) |
36 | 25, 35 | sylbi 206 |
. . . 4
⊢ (𝑦 ∈ (𝑈↑↑1𝑜) →
𝑦 ∈ 𝑈) |
37 | 24, 36 | impbii 198 |
. . 3
⊢ (𝑦 ∈ 𝑈 ↔ 𝑦 ∈ (𝑈↑↑1𝑜)) |
38 | 37 | eqriv 2607 |
. 2
⊢ 𝑈 = (𝑈↑↑1𝑜) |
39 | 38 | eqcomi 2619 |
1
⊢ (𝑈↑↑1𝑜) = 𝑈 |