Proof of Theorem finxpreclem2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfv 1913 | . . . . . 6
⊢
Ⅎ𝑥(𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) | 
| 2 |  | nfmpo2 7515 | . . . . . . . 8
⊢
Ⅎ𝑥(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 3 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑥〈1o, 𝑋〉 | 
| 4 | 2, 3 | nffv 6915 | . . . . . . 7
⊢
Ⅎ𝑥((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) | 
| 5 |  | nfcv 2904 | . . . . . . 7
⊢
Ⅎ𝑥∅ | 
| 6 | 4, 5 | nfne 3042 | . . . . . 6
⊢
Ⅎ𝑥((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅ | 
| 7 | 1, 6 | nfim 1895 | . . . . 5
⊢
Ⅎ𝑥((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) | 
| 8 |  | nfv 1913 | . . . . . . 7
⊢
Ⅎ𝑛 𝑥 = 𝑋 | 
| 9 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑛(𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) | 
| 10 |  | nfmpo1 7514 | . . . . . . . . . 10
⊢
Ⅎ𝑛(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 11 |  | nfcv 2904 | . . . . . . . . . 10
⊢
Ⅎ𝑛〈1o, 𝑋〉 | 
| 12 | 10, 11 | nffv 6915 | . . . . . . . . 9
⊢
Ⅎ𝑛((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) | 
| 13 |  | nfcv 2904 | . . . . . . . . 9
⊢
Ⅎ𝑛∅ | 
| 14 | 12, 13 | nfne 3042 | . . . . . . . 8
⊢
Ⅎ𝑛((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅ | 
| 15 | 9, 14 | nfim 1895 | . . . . . . 7
⊢
Ⅎ𝑛((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅) | 
| 16 | 8, 15 | nfim 1895 | . . . . . 6
⊢
Ⅎ𝑛(𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅)) | 
| 17 |  | 1onn 8679 | . . . . . . 7
⊢
1o ∈ ω | 
| 18 | 17 | elexi 3502 | . . . . . 6
⊢
1o ∈ V | 
| 19 |  | df-ov 7435 | . . . . . . . . . 10
⊢
(1o(𝑛
∈ ω, 𝑥 ∈ V
↦ if((𝑛 =
1o ∧ 𝑥
∈ 𝑈), ∅,
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) | 
| 20 |  | 0ex 5306 | . . . . . . . . . . . . . . . 16
⊢ ∅
∈ V | 
| 21 |  | opex 5468 | . . . . . . . . . . . . . . . . 17
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ∈ V | 
| 22 |  | opex 5468 | . . . . . . . . . . . . . . . . 17
⊢
〈𝑛, 𝑥〉 ∈ V | 
| 23 | 21, 22 | ifex 4575 | . . . . . . . . . . . . . . . 16
⊢ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ∈ V | 
| 24 | 20, 23 | ifex 4575 | . . . . . . . . . . . . . . 15
⊢ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V | 
| 25 | 24 | csbex 5310 | . . . . . . . . . . . . . 14
⊢
⦋𝑋 /
𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V | 
| 26 | 25 | csbex 5310 | . . . . . . . . . . . . 13
⊢
⦋1o / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ∈ V | 
| 27 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) = (𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 28 | 27 | ovmpos 7582 | . . . . . . . . . . . . 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 480 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → (1o(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) = ⦋1o / 𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 31 |  | csbeq1a 3912 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑋 → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 32 |  | csbeq1a 3912 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = 1o →
⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 33 | 31, 32 | sylan9eqr 2798 | . . . . . . . . . . . . . 14
⊢ ((𝑛 = 1o ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉))) | 
| 35 |  | eleq1 2828 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑋 → (𝑥 ∈ 𝑈 ↔ 𝑋 ∈ 𝑈)) | 
| 36 | 35 | notbid 318 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑋 → (¬ 𝑥 ∈ 𝑈 ↔ ¬ 𝑋 ∈ 𝑈)) | 
| 37 | 36 | biimprcd 250 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → ¬ 𝑥 ∈ 𝑈)) | 
| 38 |  | pm3.14 997 | . . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑛 = 1o ∨
¬ 𝑥 ∈ 𝑈) → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)) | 
| 39 | 38 | olcs 876 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑥 ∈ 𝑈 → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈)) | 
| 40 | 37, 39 | syl6 35 | . . . . . . . . . . . . . . . . 17
⊢ (¬
𝑋 ∈ 𝑈 → (𝑥 = 𝑋 → ¬ (𝑛 = 1o ∧ 𝑥 ∈ 𝑈))) | 
| 41 |  | iffalse 4533 | . . . . . . . . . . . . . . . . 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 406 | . . . . . . . . . . . . . . 15
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) = if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) | 
| 44 |  | ifeqor 4576 | . . . . . . . . . . . . . . . . 17
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 ∨
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) | 
| 45 |  | vuniex 7760 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ∪ 𝑛
∈ V | 
| 46 |  | fvex 6918 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(1st ‘𝑥) ∈ V | 
| 47 | 45, 46 | opnzi 5478 | . . . . . . . . . . . . . . . . . . . 20
⊢
〈∪ 𝑛, (1st ‘𝑥)〉 ≠ ∅ | 
| 48 | 47 | neii 2941 | . . . . . . . . . . . . . . . . . . 19
⊢  ¬
〈∪ 𝑛, (1st ‘𝑥)〉 = ∅ | 
| 49 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 →
(if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅ ↔ 〈∪ 𝑛,
(1st ‘𝑥)〉 = ∅)) | 
| 50 | 48, 49 | mtbiri 327 | . . . . . . . . . . . . . . . . . 18
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 →
¬ if(𝑥 ∈ (V
× 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) | 
| 51 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑛 ∈ V | 
| 52 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V | 
| 53 | 51, 52 | opnzi 5478 | . . . . . . . . . . . . . . . . . . . 20
⊢
〈𝑛, 𝑥〉 ≠
∅ | 
| 54 | 53 | neii 2941 | . . . . . . . . . . . . . . . . . . 19
⊢  ¬
〈𝑛, 𝑥〉 = ∅ | 
| 55 |  | eqeq1 2740 | . . . . . . . . . . . . . . . . . . 19
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉 → (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅ ↔ 〈𝑛, 𝑥〉 = ∅)) | 
| 56 | 54, 55 | mtbiri 327 | . . . . . . . . . . . . . . . . . 18
⊢ (if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉 → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) | 
| 57 | 50, 56 | jaoi 857 | . . . . . . . . . . . . . . . . 17
⊢
((if(𝑥 ∈ (V
× 𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈∪
𝑛, (1st
‘𝑥)〉 ∨
if(𝑥 ∈ (V ×
𝑈), 〈∪ 𝑛,
(1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = 〈𝑛, 𝑥〉) → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) | 
| 58 | 44, 57 | mp1i 13 | . . . . . . . . . . . . . . . 16
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → ¬ if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) = ∅) | 
| 59 | 58 | neqned 2946 | . . . . . . . . . . . . . . 15
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉) ≠ ∅) | 
| 60 | 43, 59 | eqnetrd 3007 | . . . . . . . . . . . . . 14
⊢ ((¬
𝑋 ∈ 𝑈 ∧ 𝑥 = 𝑋) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) | 
| 61 | 60 | adantrl 716 | . . . . . . . . . . . . 13
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋)) → if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) | 
| 62 | 34, 61 | eqnetrrd 3008 | . . . . . . . . . . . 12
⊢ ((¬
𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋)) → ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) | 
| 63 | 62 | adantl 481 | . . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → ⦋1o /
𝑛⦌⦋𝑋 / 𝑥⦌if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)) ≠ ∅) | 
| 64 | 30, 63 | eqnetrd 3007 | . . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (¬ 𝑋 ∈ 𝑈 ∧ (𝑛 = 1o ∧ 𝑥 = 𝑋))) → (1o(𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))𝑋) ≠ ∅) | 
| 65 | 19, 64 | eqnetrrid 3015 | . . . . . . . . 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 419 | . . . . . 6
⊢ (𝑛 = 1o → (𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅))) | 
| 69 | 16, 18, 68 | vtoclef 3562 | . . . . 5
⊢ (𝑥 = 𝑋 → ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉) ≠
∅)) | 
| 70 | 7, 69 | vtoclefex 37336 | . . . 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 2995 | . 2
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ∅ ≠ ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉)) | 
| 73 | 72 | neneqd 2944 | 1
⊢ ((𝑋 ∈ V ∧ ¬ 𝑋 ∈ 𝑈) → ¬ ∅ = ((𝑛 ∈ ω, 𝑥 ∈ V ↦ if((𝑛 = 1o ∧ 𝑥 ∈ 𝑈), ∅, if(𝑥 ∈ (V × 𝑈), 〈∪ 𝑛, (1st ‘𝑥)〉, 〈𝑛, 𝑥〉)))‘〈1o, 𝑋〉)) |