Step | Hyp | Ref
| Expression |
1 | | eleq1 2676 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 ∈ ω ↔ 𝑁 ∈ ω)) |
2 | | eleq2 2677 |
. . . . 5
⊢ (𝑛 = 𝑁 → (1𝑜 ∈ 𝑛 ↔ 1𝑜
∈ 𝑁)) |
3 | 1, 2 | anbi12d 743 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ↔ (𝑁 ∈ ω ∧
1𝑜 ∈ 𝑁))) |
4 | | anass 679 |
. . . . . . . . 9
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑦 ∈ (V × 𝑈)) ↔ (𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) |
5 | | nfv 1830 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥(𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) |
6 | | finxpreclem5.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐹 = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
7 | | nfmpt22 6621 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
8 | 6, 7 | nfcxfr 2749 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥𝐹 |
9 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥〈𝑛, 𝑦〉 |
10 | 8, 9 | nfrdg 7397 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥rec(𝐹, 〈𝑛, 𝑦〉) |
11 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥𝑛 |
12 | 10, 11 | nffv 6110 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛) |
13 | 12 | nfeq2 2766 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥∅ =
(rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛) |
14 | 13 | nfn 1768 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥 ¬
∅ = (rec(𝐹,
〈𝑛, 𝑦〉)‘𝑛) |
15 | 5, 14 | nfim 1813 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)) |
16 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → (𝑥 ∈ (V × 𝑈) ↔ 𝑦 ∈ (V × 𝑈))) |
17 | 16 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (¬ 𝑥 ∈ (V × 𝑈) ↔ ¬ 𝑦 ∈ (V × 𝑈))) |
18 | 17 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → ((1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈)) ↔ (1𝑜 ∈
𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) |
19 | 18 | anbi2d 736 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) ↔ (𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))))) |
20 | | opeq2 4341 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑦 → 〈𝑛, 𝑥〉 = 〈𝑛, 𝑦〉) |
21 | | rdgeq2 7395 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝑛, 𝑥〉 = 〈𝑛, 𝑦〉 → rec(𝐹, 〈𝑛, 𝑥〉) = rec(𝐹, 〈𝑛, 𝑦〉)) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑦 → rec(𝐹, 〈𝑛, 𝑥〉) = rec(𝐹, 〈𝑛, 𝑦〉)) |
23 | 22 | fveq1d 6105 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)) |
24 | 23 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (∅ = (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) ↔ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))) |
25 | 24 | notbid 307 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → (¬ ∅ = (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) ↔ ¬ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))) |
26 | 19, 25 | imbi12d 333 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (((𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ¬ ∅ =
(rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛)) ↔ ((𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ ∅ =
(rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)))) |
27 | | anass 679 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) ↔ (𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈)))) |
28 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑛 ∈ V |
29 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = ∅ → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = (rec(𝐹, 〈𝑛, 𝑥〉)‘∅)) |
30 | 29 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = ∅ → ((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉 ↔ (rec(𝐹, 〈𝑛, 𝑥〉)‘∅) = 〈𝑛, 𝑥〉)) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑜 → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜)) |
32 | 31 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑜 → ((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉 ↔ (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜) = 〈𝑛, 𝑥〉)) |
33 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = suc 𝑜 → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜)) |
34 | 33 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = suc 𝑜 → ((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉 ↔ (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = 〈𝑛, 𝑥〉)) |
35 | | opex 4859 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
〈𝑛, 𝑥〉 ∈ V |
36 | 35 | rdg0 7404 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(rec(𝐹, 〈𝑛, 𝑥〉)‘∅) = 〈𝑛, 𝑥〉 |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘∅) = 〈𝑛, 𝑥〉) |
38 | | nnon 6963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑜 ∈ ω → 𝑜 ∈ On) |
39 | | rdgsuc 7407 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑜 ∈ On → (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = (𝐹‘(rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑜 ∈ ω →
(rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = (𝐹‘(rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜))) |
41 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜) = 〈𝑛, 𝑥〉 → (𝐹‘(rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜)) = (𝐹‘〈𝑛, 𝑥〉)) |
42 | 40, 41 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑜 ∈ ω ∧ (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜) = 〈𝑛, 𝑥〉) → (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = (𝐹‘〈𝑛, 𝑥〉)) |
43 | 6 | finxpreclem5 32408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) → (¬ 𝑥 ∈ (V × 𝑈) → (𝐹‘〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉)) |
44 | 43 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (𝐹‘〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
45 | 42, 44 | sylan9eq 2664 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑜 ∈ ω ∧ (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜) = 〈𝑛, 𝑥〉) ∧ ((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = 〈𝑛, 𝑥〉) |
46 | 45 | expl 646 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑜 ∈ ω →
(((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜) = 〈𝑛, 𝑥〉 ∧ ((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = 〈𝑛, 𝑥〉)) |
47 | 46 | expcomd 453 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑜 ∈ ω → (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → ((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑜) = 〈𝑛, 𝑥〉 → (rec(𝐹, 〈𝑛, 𝑥〉)‘suc 𝑜) = 〈𝑛, 𝑥〉))) |
48 | 30, 32, 34, 37, 47 | finds2 6986 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ω → (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉)) |
49 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → (𝑛 ∈ ω ↔ 𝑚 ∈ ω)) |
50 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 = 𝑚 → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚)) |
51 | 50 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑛 = 𝑚 → ((rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉 ↔ (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉)) |
52 | 51 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 𝑚 → ((((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉) ↔ (((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉))) |
53 | 49, 52 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 𝑚 → ((𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉)) ↔ (𝑚 ∈ ω → (((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑚) = 〈𝑛, 𝑥〉)))) |
54 | 48, 53 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉))) |
55 | 54 | equcoms 1934 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (𝑛 ∈ ω → (((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉))) |
56 | 28, 55 | vtocle 3255 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ω → (((𝑛 ∈ ω ∧
1𝑜 ∈ 𝑛) ∧ ¬ 𝑥 ∈ (V × 𝑈)) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉)) |
57 | 27, 56 | syl5bir 232 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ ω → ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉)) |
58 | 57 | anabsi5 854 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) = 〈𝑛, 𝑥〉) |
59 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑥 ∈ V |
60 | 28, 59 | opnzi 4869 |
. . . . . . . . . . . . . . . . . 18
⊢
〈𝑛, 𝑥〉 ≠
∅ |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → 〈𝑛, 𝑥〉 ≠ ∅) |
62 | 58, 61 | eqnetrd 2849 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛) ≠ ∅) |
63 | 62 | necomd 2837 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ∅ ≠ (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛)) |
64 | 63 | neneqd 2787 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑥 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, 〈𝑛, 𝑥〉)‘𝑛)) |
65 | 15, 26, 64 | chvar 2250 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)) |
66 | 65 | intnand 953 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ω ∧
(1𝑜 ∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))) |
67 | 66 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) → ¬ (𝑛 ∈ ω ∧ ∅ =
(rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))) |
68 | | abid 2598 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))} ↔ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))) |
69 | | opeq1 4340 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑁 → 〈𝑛, 𝑦〉 = 〈𝑁, 𝑦〉) |
70 | | rdgeq2 7395 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(〈𝑛, 𝑦〉 = 〈𝑁, 𝑦〉 → rec(𝐹, 〈𝑛, 𝑦〉) = rec(𝐹, 〈𝑁, 𝑦〉)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑁 → rec(𝐹, 〈𝑛, 𝑦〉) = rec(𝐹, 〈𝑁, 𝑦〉)) |
72 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑁 → 𝑛 = 𝑁) |
73 | 71, 72 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑁 → (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛) = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁)) |
74 | 73 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑁 → (∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛) ↔ ∅ = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁))) |
75 | 1, 74 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)) ↔ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁)))) |
76 | 75 | abbidv 2728 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑁 → {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))} = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁))}) |
77 | 6 | dffinxpf 32398 |
. . . . . . . . . . . . . . 15
⊢ (𝑈↑↑𝑁) = {𝑦 ∣ (𝑁 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑁, 𝑦〉)‘𝑁))} |
78 | 76, 77 | syl6eqr 2662 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑁 → {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))} = (𝑈↑↑𝑁)) |
79 | 78 | eleq2d 2673 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑁 → (𝑦 ∈ {𝑦 ∣ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛))} ↔ 𝑦 ∈ (𝑈↑↑𝑁))) |
80 | 68, 79 | syl5rbbr 274 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑁 → (𝑦 ∈ (𝑈↑↑𝑁) ↔ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)))) |
81 | 80 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) → (𝑦 ∈ (𝑈↑↑𝑁) ↔ (𝑛 ∈ ω ∧ ∅ = (rec(𝐹, 〈𝑛, 𝑦〉)‘𝑛)))) |
82 | 67, 81 | mtbird 314 |
. . . . . . . . . 10
⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈)))) → ¬ 𝑦 ∈ (𝑈↑↑𝑁)) |
83 | 82 | ex 449 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ (1𝑜
∈ 𝑛 ∧ ¬ 𝑦 ∈ (V × 𝑈))) → ¬ 𝑦 ∈ (𝑈↑↑𝑁))) |
84 | 4, 83 | syl5bi 231 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) ∧ ¬ 𝑦 ∈ (V × 𝑈)) → ¬ 𝑦 ∈ (𝑈↑↑𝑁))) |
85 | 84 | expdimp 452 |
. . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛)) → (¬
𝑦 ∈ (V × 𝑈) → ¬ 𝑦 ∈ (𝑈↑↑𝑁))) |
86 | 85 | con4d 113 |
. . . . . 6
⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛)) → (𝑦 ∈ (𝑈↑↑𝑁) → 𝑦 ∈ (V × 𝑈))) |
87 | 86 | ssrdv 3574 |
. . . . 5
⊢ ((𝑛 = 𝑁 ∧ (𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛)) → (𝑈↑↑𝑁) ⊆ (V × 𝑈)) |
88 | 87 | ex 449 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑛 ∈ ω ∧ 1𝑜
∈ 𝑛) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))) |
89 | 3, 88 | sylbird 249 |
. . 3
⊢ (𝑛 = 𝑁 → ((𝑁 ∈ ω ∧ 1𝑜
∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))) |
90 | 89 | vtocleg 3252 |
. 2
⊢ (𝑁 ∈ ω → ((𝑁 ∈ ω ∧
1𝑜 ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈))) |
91 | 90 | anabsi5 854 |
1
⊢ ((𝑁 ∈ ω ∧
1𝑜 ∈ 𝑁) → (𝑈↑↑𝑁) ⊆ (V × 𝑈)) |