ssetex - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > ssetex		GIF version

Theorem ssetex 4745

Description: The subset relationship is a set. (Contributed by SF, 6-Jan-2015.)

**Assertion**
Ref	Expression
ssetex	⊢ S ∈ V

**Proof of Theorem ssetex**
Step	Hyp	Ref	Expression
1		dfsset2 4744	. 2 ⊢ S = ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k S_k )
2		vvex 4110	. . . . . . . 8 ⊢ V ∈ V
3	2, 2	xpkex 4290	. . . . . . 7 ⊢ (V ×_k V) ∈ V
4	3, 2	xpkex 4290	. . . . . 6 ⊢ ((V ×_k V) ×_k V) ∈ V
5		setconslem5 4736	. . . . . . 7 ⊢ ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c) ∈ V
6	5	cnvkex 4288	. . . . . 6 ⊢ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c) ∈ V
7	4, 6	inex 4106	. . . . 5 ⊢ (((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) ∈ V
8		ssetkex 4295	. . . . 5 ⊢ S_k ∈ V
9	7, 8	imakex 4301	. . . 4 ⊢ ((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k S_k ) ∈ V
10	9	uni1ex 4294	. . 3 ⊢ ⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k S_k ) ∈ V
11	10	uni1ex 4294	. 2 ⊢ ⋃₁⋃₁((((V ×_k V) ×_k V) ∩ ^◡_k ∼ (( Ins3_k SI_k SI_k S_k ⊕ Ins2_k ( Ins3_k ( S_k ∘_k SI_k ^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V)))) ∪ Ins2_k (( Ins2_k S_k ∩ Ins3_k SI_k ∼ (( Ins2_k S_k ⊕ Ins3_k ((^◡_kImage_k((Image_k(( Ins3_k ∼ (( Ins3_k S_k ∩ Ins2_k S_k ) “_k 𝒫₁𝒫₁1_c) ∖ (( Ins2_k Ins2_k S_k ⊕ ( Ins2_k Ins3_k S_k ∪ Ins3_k SI_k SI_k S_k )) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c) ∩ ( Nn ×_k V)) ∪ ( I_k ∩ ( ∼ Nn ×_k V))) ∘_k S_k ) ∪ ({{0_c}} ×_k V))) “_k 𝒫₁𝒫₁1_c)) “_k 𝒫₁𝒫₁1_c))) “_k 𝒫₁𝒫₁𝒫₁𝒫₁1_c)) “_k S_k ) ∈ V
12	1, 11	eqeltri 2423	1 ⊢ S ∈ V

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 1710 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 {csn 3738 ⋃₁cuni1 4134 1_cc1c 4135 𝒫₁cpw1 4136 ×_k cxpk 4175 ^◡_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 ∘_k ccomk 4181 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184 I_k cidk 4185 Nn cnnc 4374 0_cc0c 4375 S csset 4720

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This proof depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-addc 4379 df-nnc 4380 df-phi 4566 df-op 4567 df-opab 4624 df-sset 4726

This theorem is used by: idex 5505 imageexg 5801 mptexlem 5811 mpt2exlem 5812 cupex 5817 composeex 5821 disjex 5824 addcfnex 5825 funsex 5829 crossex 5851 pw1fnex 5853 domfnex 5871 ranfnex 5872 clos1ex 5877 transex 5911 refex 5912 antisymex 5913 connexex 5914 foundex 5915 extex 5916 symex 5917 ssetpov 5945 qsexg 5983 enprmaplem1 6077 nenpw1pwlem1 6085 lecex 6116 mucex 6134 ovcelem1 6172 ceex 6175 tcfnex 6245 nmembers1lem1 6269 nchoicelem11 6300 nchoicelem16 6305 nchoicelem18 6307

W3C validator