Proof of Theorem ssetex
Step | Hyp | Ref
| Expression |
1 | | dfsset2 4743 |
. 2
⊢ S = ⋃1⋃1((((V
×k V) ×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k Sk ) |
2 | | vvex 4109 |
. . . . . . . 8
⊢ V ∈ V |
3 | 2, 2 | xpkex 4289 |
. . . . . . 7
⊢ (V
×k V) ∈
V |
4 | 3, 2 | xpkex 4289 |
. . . . . 6
⊢ ((V
×k V) ×k V) ∈ V |
5 | | setconslem5 4735 |
. . . . . . 7
⊢ ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c) ∈
V |
6 | 5 | cnvkex 4287 |
. . . . . 6
⊢ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c) ∈
V |
7 | 4, 6 | inex 4105 |
. . . . 5
⊢ (((V
×k V) ×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) ∈
V |
8 | | ssetkex 4294 |
. . . . 5
⊢ Sk ∈
V |
9 | 7, 8 | imakex 4300 |
. . . 4
⊢ ((((V
×k V) ×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k Sk ) ∈ V |
10 | 9 | uni1ex 4293 |
. . 3
⊢
⋃1((((V ×k V)
×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k Sk ) ∈ V |
11 | 10 | uni1ex 4293 |
. 2
⊢
⋃1⋃1((((V ×k V)
×k V) ∩ ◡k ∼ (( Ins3k SIk SIk Sk ⊕ Ins2k ( Ins3k ( Sk ∘k SIk ◡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)))) ∪ Ins2k (( Ins2k Sk ∩
Ins3k SIk
∼ (( Ins2k Sk ⊕ Ins3k
((◡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 Sk ) ∪ ({{0c}} ×k
V))) “k ℘1℘11c)) “k ℘1℘11c))) “k ℘1℘1℘1℘11c)) “k Sk ) ∈ V |
12 | 1, 11 | eqeltri 2423 |
1
⊢ S ∈
V |