Proof of Theorem nncex
Step | Hyp | Ref
| Expression |
1 | | dfnnc2 4395 |
. 2
⊢ Nn = ∩({x ∣
0c ∈ x} ∖ (( Sk ∖ ( Sk ∘k SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c)))
“k 1c)) |
2 | | setswithex 4322 |
. . . 4
⊢ {x ∣
0c ∈ x} ∈
V |
3 | | ssetkex 4294 |
. . . . . 6
⊢ Sk ∈
V |
4 | | addcexlem 4382 |
. . . . . . . . . 10
⊢ ( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) ∈ V |
5 | | 1cex 4142 |
. . . . . . . . . . . 12
⊢
1c ∈
V |
6 | 5 | pw1ex 4303 |
. . . . . . . . . . 11
⊢ ℘11c ∈ V |
7 | 6 | pw1ex 4303 |
. . . . . . . . . 10
⊢ ℘1℘11c ∈ V |
8 | 4, 7 | imakex 4300 |
. . . . . . . . 9
⊢ (( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c) ∈ V |
9 | 8 | imagekex 4312 |
. . . . . . . 8
⊢
Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c) ∈ V |
10 | 9 | sikex 4297 |
. . . . . . 7
⊢ SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c) ∈ V |
11 | 3, 10 | cokex 4310 |
. . . . . 6
⊢ ( Sk ∘k SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c)) ∈ V |
12 | 3, 11 | difex 4107 |
. . . . 5
⊢ ( Sk ∖ ( Sk ∘k SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c))) ∈ V |
13 | 12, 5 | imakex 4300 |
. . . 4
⊢ (( Sk ∖ ( Sk ∘k SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c)))
“k 1c) ∈ V |
14 | 2, 13 | difex 4107 |
. . 3
⊢ ({x ∣
0c ∈ x} ∖ (( Sk ∖ ( Sk ∘k SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c)))
“k 1c)) ∈ V |
15 | 14 | intex 4320 |
. 2
⊢ ∩({x ∣ 0c ∈ x} ∖ (( Sk ∖ ( Sk ∘k SIk Imagek(( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c))
“k ℘1℘11c)))
“k 1c)) ∈ V |
16 | 1, 15 | eqeltri 2423 |
1
⊢ Nn ∈
V |