Proof of Theorem finxpreclem2
Step | Hyp | Ref
| Expression |
1 | | nfv 1921 |
. . . . . 6
⊢
Ⅎ𝑥(𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) |
2 | | nfmpo2 7249 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
3 | | nfcv 2899 |
. . . . . . . 8
⊢
Ⅎ𝑥〈1o, 𝑋〉 |
4 | 2, 3 | nffv 6684 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) |
5 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑥∅ |
6 | 4, 5 | nfne 3034 |
. . . . . 6
⊢
Ⅎ𝑥((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅ |
7 | 1, 6 | nfim 1903 |
. . . . 5
⊢
Ⅎ𝑥((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) |
8 | | nfv 1921 |
. . . . . . 7
⊢
Ⅎ𝑛 𝑥 = 𝑋 |
9 | | nfv 1921 |
. . . . . . . 8
⊢
Ⅎ𝑛(𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) |
10 | | nfmpo1 7248 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
11 | | nfcv 2899 |
. . . . . . . . . 10
⊢
Ⅎ𝑛〈1o, 𝑋〉 |
12 | 10, 11 | nffv 6684 |
. . . . . . . . 9
⊢
Ⅎ𝑛((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) |
13 | | nfcv 2899 |
. . . . . . . . 9
⊢
Ⅎ𝑛∅ |
14 | 12, 13 | nfne 3034 |
. . . . . . . 8
⊢
Ⅎ𝑛((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅ |
15 | 9, 14 | nfim 1903 |
. . . . . . 7
⊢
Ⅎ𝑛((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) |
16 | 8, 15 | nfim 1903 |
. . . . . 6
⊢
Ⅎ𝑛(𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅)) |
17 | | 1onn 8296 |
. . . . . . 7
⊢
1o ∈ ω |
18 | 17 | elexi 3417 |
. . . . . 6
⊢
1o ∈ V |
19 | | df-ov 7173 |
. . . . . . . . . 10
⊢
(1o(𝑛
∈ ω, 𝑥 ∈ V
↦ if((𝑛 =
1o ∧ 𝑥
∈ 𝑈), ∅,
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) |
20 | | 0ex 5175 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ V |
21 | | opex 5322 |
. . . . . . . . . . . . . . . . 17
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ∈ V |
22 | | opex 5322 |
. . . . . . . . . . . . . . . . 17
⊢
〈𝑛, 𝑥〉 ∈ V |
23 | 21, 22 | ifex 4464 |
. . . . . . . . . . . . . . . 16
⊢ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ∈ V |
24 | 20, 23 | ifex 4464 |
. . . . . . . . . . . . . . 15
⊢ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
25 | 24 | csbex 5179 |
. . . . . . . . . . . . . 14
⊢
⦋𝑋 /
𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
26 | 25 | csbex 5179 |
. . . . . . . . . . . . 13
⊢
⦋1o / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V |
27 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
28 | 27 | ovmpos 7313 |
. . . . . . . . . . . . 13
⊢
((1o ∈ ω ∧ 𝑋 ∈ V ∧ ⦋1o
/ 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V) →
(1o(𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1o / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
29 | 17, 26, 28 | mp3an13 1453 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ V →
(1o(𝑛 ∈
ω, 𝑥 ∈ V ↦
if((𝑛 = 1o ∧
𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1o / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
30 | 29 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → (1o(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1o / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
31 | | csbeq1a 3804 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
32 | | csbeq1a 3804 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 1o →
⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
33 | 31, 32 | sylan9eqr 2795 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 = 1o ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
34 | 33 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
35 | | eleq1 2820 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) |
36 | 35 | notbid 321 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) |
37 | 36 | biimprcd 253 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → ¬ 𝑥 ∈ 𝑈)) |
38 | | pm3.14 995 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑛 = 1o ∨
¬ 𝑥 ∈ 𝑈) → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)) |
39 | 38 | olcs 875 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 ∈ 𝑈 → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)) |
40 | 37, 39 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈))) |
41 | | iffalse 4423 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
(𝑛 = 1o ∧
𝑥 ∈ 𝑈) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
42 | 40, 41 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) |
43 | 42 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) |
44 | | ifeqor 4465 |
. . . . . . . . . . . . . . . . 17
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 ∨
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) |
45 | | vuniex 7483 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝑛
∈ V |
46 | | fvex 6687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑥) ∈ V |
47 | 45, 46 | opnzi 5332 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ≠ ∅ |
48 | 47 | neii 2936 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
〈∪ 𝑛, (1st ‘𝑥)〉 = ∅ |
49 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 →
(if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅ ↔ 〈∪ 𝑛,
(1st ‘𝑥)〉 = ∅)) |
50 | 48, 49 | mtbiri 330 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 →
¬ if(𝑥 ∈ (V
× 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
51 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V |
52 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
53 | 51, 52 | opnzi 5332 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈𝑛, 𝑥〉 ≠
∅ |
54 | 53 | neii 2936 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
〈𝑛, 𝑥〉 = ∅ |
55 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉 → (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅ ↔ 〈𝑛, 𝑥〉 = ∅)) |
56 | 54, 55 | mtbiri 330 |
. . . . . . . . . . . . . . . . . 18
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉 → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
57 | 50, 56 | jaoi 856 |
. . . . . . . . . . . . . . . . 17
⊢
((if(𝑥 ∈ (V
× 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 ∨
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
58 | 44, 57 | mp1i 13 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) |
59 | 58 | neqned 2941 |
. . . . . . . . . . . . . . 15
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ≠ ∅) |
60 | 43, 59 | eqnetrd 3001 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
61 | 60 | adantrl 716 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
62 | 34, 61 | eqnetrrd 3002 |
. . . . . . . . . . . 12
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋)) → ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
63 | 62 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) |
64 | 30, 63 | eqnetrd 3001 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → (1o(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) ≠ ∅) |
65 | 19, 64 | eqnetrrid 3009 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) |
66 | 65 | ancom2s 650 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ ((𝑛 = 1o ∧ 𝑥 = 𝑋) ∧ ¬ 𝑋 ∈ 𝑈)) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) |
67 | 66 | an12s 649 |
. . . . . . 7
⊢ (((𝑛 = 1o ∧ 𝑥 = 𝑋) ∧ (𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈)) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) |
68 | 67 | exp31 423 |
. . . . . 6
⊢ (𝑛 = 1o → (𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅))) |
69 | 16, 18, 68 | vtoclef 3488 |
. . . . 5
⊢ (𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅)) |
70 | 7, 69 | vtoclefex 35128 |
. . . 4
⊢ (𝑋 ∈ V → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅)) |
71 | 70 | anabsi5 669 |
. . 3
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) |
72 | 71 | necomd 2989 |
. 2
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ∅ ≠ ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉)) |
73 | 72 | neneqd 2939 |
1
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ¬ ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉)) |