Proof of Theorem proj1exg
Step | Hyp | Ref
| Expression |
1 | | dfproj12 4576 |
. 2
⊢ Proj1 A = (◡kImagek((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) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) “k A) |
2 | | addcexlem 4382 |
. . . . . . . . 9
⊢ ( Ins3k ∼ (( Ins3k Sk ∩ Ins2k Sk ) “k ℘1℘11c) ∖ (( Ins2k Ins2k Sk ⊕ ( Ins2k Ins3k Sk ∪ Ins3k SIk SIk Sk )) “k ℘1℘1℘1℘11c)) ∈ V |
3 | | 1cex 4142 |
. . . . . . . . . . 11
⊢
1c ∈
V |
4 | 3 | pw1ex 4303 |
. . . . . . . . . 10
⊢ ℘11c ∈ V |
5 | 4 | pw1ex 4303 |
. . . . . . . . 9
⊢ ℘1℘11c ∈ V |
6 | 2, 5 | imakex 4300 |
. . . . . . . 8
⊢ (( 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 |
7 | 6 | imagekex 4312 |
. . . . . . 7
⊢
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 |
8 | | nncex 4396 |
. . . . . . . 8
⊢ Nn ∈
V |
9 | | vvex 4109 |
. . . . . . . 8
⊢ V ∈ V |
10 | 8, 9 | xpkex 4289 |
. . . . . . 7
⊢ ( Nn ×k V) ∈ V |
11 | 7, 10 | inex 4105 |
. . . . . 6
⊢
(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) ∩ ( Nn ×k V)) ∈ V |
12 | | idkex 4314 |
. . . . . . 7
⊢
Ik ∈ V |
13 | 8 | complex 4104 |
. . . . . . . 8
⊢ ∼ Nn ∈
V |
14 | 13, 9 | xpkex 4289 |
. . . . . . 7
⊢ ( ∼ Nn ×k V) ∈ V |
15 | 12, 14 | inex 4105 |
. . . . . 6
⊢ (
Ik ∩ ( ∼ Nn
×k V)) ∈
V |
16 | 11, 15 | unex 4106 |
. . . . 5
⊢
((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) ∩ ( Nn ×k V)) ∪ (
Ik ∩ ( ∼ Nn
×k V))) ∈
V |
17 | 16 | imagekex 4312 |
. . . 4
⊢
Imagek((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) ∩ ( Nn ×k V)) ∪ (
Ik ∩ ( ∼ Nn
×k V))) ∈
V |
18 | 17 | cnvkex 4287 |
. . 3
⊢ ◡kImagek((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) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∈ V |
19 | | imakexg 4299 |
. . 3
⊢ ((◡kImagek((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) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) ∈ V ∧
A ∈ V) → (◡kImagek((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) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) “k A) ∈ V) |
20 | 18, 19 | mpan 651 |
. 2
⊢ (A ∈ V → (◡kImagek((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) ∩ ( Nn
×k V)) ∪ ( Ik ∩ ( ∼ Nn
×k V))) “k A) ∈ V) |
21 | 1, 20 | syl5eqel 2437 |
1
⊢ (A ∈ V → Proj1
A ∈ V) |