Proof of Theorem finxpreclem2
Step | Hyp | Ref
| Expression |
1 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑥(𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) |
2 | | nfmpt22 6723 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
3 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑥〈1𝑜, 𝑋〉 |
4 | 2, 3 | nffv 6198 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) |
5 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑥∅ |
6 | 4, 5 | nfne 2894 |
. . . . . 6
⊢
Ⅎ𝑥((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅ |
7 | 1, 6 | nfim 1825 |
. . . . 5
⊢
Ⅎ𝑥((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅) |
8 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑥 = 𝑋 |
9 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) |
10 | | nfmpt21 6722 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
11 | | nfcv 2764 |
. . . . . . . . . 10
⊢
Ⅎ𝑛〈1𝑜, 𝑋〉 |
12 | 10, 11 | nffv 6198 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) |
13 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑛∅ |
14 | 12, 13 | nfne 2894 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅ |
15 | 9, 14 | nfim 1825 |
. . . . . . 7
⊢
Ⅎ𝑛((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅) |
16 | 8, 15 | nfim 1825 |
. . . . . 6
⊢
Ⅎ𝑛(𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅)) |
17 | | 1onn 7719 |
. . . . . . 7
⊢
1𝑜 ∈ ω |
18 | 17 | elexi 3213 |
. . . . . 6
⊢
1𝑜 ∈ V |
19 | | df-ov 6653 |
. . . . . . . . . 10
⊢
(1𝑜(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) |
20 | | 0ex 4790 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ V |
21 | | opex 4932 |
. . . . . . . . . . . . . . . . 17
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ∈ V |
22 | | opex 4932 |
. . . . . . . . . . . . . . . . 17
⊢
〈𝑛, 𝑥〉 ∈ V |
23 | 21, 22 | ifex 4156 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ∈ V |
24 | 20, 23 | ifex 4156 |
. . . . . . . . . . . . . . 15
⊢ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
25 | 24 | csbex 4793 |
. . . . . . . . . . . . . 14
⊢
⦋𝑋 /
𝑥⦌if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
26 | 25 | csbex 4793 |
. . . . . . . . . . . . 13
⊢
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
27 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
28 | 27 | ovmpt2s 6784 |
. . . . . . . . . . . . 13
⊢
((1𝑜 ∈ ω ∧ 𝑋 ∈ V ∧
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V) →
(1𝑜(𝑛
∈ ω, 𝑥 ∈ V
↦ if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1𝑜 /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
29 | 17, 26, 28 | mp3an13 1415 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ V →
(1𝑜(𝑛
∈ ω, 𝑥 ∈ V
↦ if((𝑛 =
1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1𝑜 /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
30 | 29 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋))) → (1𝑜(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1𝑜 /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
31 | | csbeq1a 3542 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
32 | | csbeq1a 3542 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1𝑜 →
⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) =
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
33 | 31, 32 | sylan9eqr 2678 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 = 1𝑜 ∧
𝑥 = 𝑋) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) =
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
34 | 33 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) =
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
35 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) |
36 | 35 | notbid 308 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) |
37 | 36 | biimprcd 240 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → ¬ 𝑥 ∈ 𝑈)) |
38 | | pm3.14 523 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑛 = 1𝑜
∨ ¬ 𝑥 ∈ 𝑈) → ¬ (𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈)) |
39 | 38 | olcs 410 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 ∈ 𝑈 → ¬ (𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈)) |
40 | 37, 39 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → ¬ (𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈))) |
41 | | iffalse 4095 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑛 = 1𝑜
∧ 𝑥 ∈ 𝑈) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
42 | 40, 41 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
43 | 42 | imp 445 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
44 | | ifeqor 4132 |
. . . . . . . . . . . . . . . . 17
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 ∨
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
45 | | vuniex 6954 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝑛
∈ V |
46 | | fvex 6201 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑥) ∈ V |
47 | 45, 46 | opnzi 4943 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ≠ ∅ |
48 | 47 | neii 2796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
〈∪ 𝑛, (1st ‘𝑥)〉 = ∅ |
49 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 →
(if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅ ↔ 〈∪ 𝑛,
(1st ‘𝑥)〉 = ∅)) |
50 | 48, 49 | mtbiri 317 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 →
¬ if(𝑥 ∈ (V
× 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
51 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V |
52 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
53 | 51, 52 | opnzi 4943 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈𝑛, 𝑥〉 ≠
∅ |
54 | 53 | neii 2796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
〈𝑛, 𝑥〉 = ∅ |
55 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉 → (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅ ↔ 〈𝑛, 𝑥〉 = ∅)) |
56 | 54, 55 | mtbiri 317 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉 → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
57 | 50, 56 | jaoi 394 |
. . . . . . . . . . . . . . . . 17
⊢
((if(𝑥 ∈ (V
× 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 ∨
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
58 | 44, 57 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
59 | 58 | neqned 2801 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ≠ ∅) |
60 | 43, 59 | eqnetrd 2861 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
61 | 60 | adantrl 752 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋)) → if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
62 | 34, 61 | eqnetrrd 2862 |
. . . . . . . . . . . 12
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋)) →
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
63 | 62 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋))) →
⦋1𝑜 / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
64 | 30, 63 | eqnetrd 2861 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋))) → (1𝑜(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) ≠ ∅) |
65 | 19, 64 | syl5eqner 2869 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1𝑜 ∧ 𝑥 = 𝑋))) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅) |
66 | 65 | ancom2s 844 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ ((𝑛 = 1𝑜 ∧
𝑥 = 𝑋) ∧ ¬ 𝑋 ∈ 𝑈)) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅) |
67 | 66 | an12s 843 |
. . . . . . 7
⊢ (((𝑛 = 1𝑜 ∧
𝑥 = 𝑋) ∧ (𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈)) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅) |
68 | 67 | exp31 630 |
. . . . . 6
⊢ (𝑛 = 1𝑜 →
(𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅))) |
69 | 16, 18, 68 | vtoclef 3281 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅)) |
70 | 7, 69 | vtoclefex 33181 |
. . . 4
⊢ (𝑋 ∈ V → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅)) |
71 | 70 | anabsi5 858 |
. . 3
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉) ≠
∅) |
72 | 71 | necomd 2849 |
. 2
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ∅ ≠ ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉)) |
73 | 72 | neneqd 2799 |
1
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ¬ ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1𝑜 ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1𝑜,
𝑋〉)) |