siexg - New Foundations Explorer

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

Theorem siexg 4753

Description: The singleton image of a set is a set. (Contributed by SF, 7-Jan-2015.)

**Assertion**
Ref	Expression
siexg	⊢ (A ∈ V → SI A ∈ V)

**Proof of Theorem siexg**
Step	Hyp	Ref	Expression
1		dfsi2 4752	. 2 ⊢ SI A = ⋃₁⋃₁((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A))
2		pw1exg 4303	. . . . 5 ⊢ (A ∈ V → 𝒫₁A ∈ V)
3		pw1exg 4303	. . . . 5 ⊢ (𝒫₁A ∈ V → 𝒫₁𝒫₁A ∈ V)
4		vvex 4110	. . . . . . . 8 ⊢ V ∈ V
5	4, 4	xpkex 4290	. . . . . . . 8 ⊢ (V ×_k V) ∈ V
6	4, 5	xpkex 4290	. . . . . . 7 ⊢ (V ×_k (V ×_k V)) ∈ V
7		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
8	6, 7	inex 4106	. . . . . 6 ⊢ ((V ×_k (V ×_k V)) ∩ ∼ (( 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
9		imakexg 4300	. . . . . 6 ⊢ ((((V ×_k (V ×_k V)) ∩ ∼ (( 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 ∧ 𝒫₁𝒫₁A ∈ V) → (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V)
10	8, 9	mpan 651	. . . . 5 ⊢ (𝒫₁𝒫₁A ∈ V → (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V)
11	2, 3, 10	3syl 18	. . . 4 ⊢ (A ∈ V → (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V)
12		sikexg 4297	. . . 4 ⊢ ((((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V → SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V)
13	5, 4	xpkex 4290	. . . . . 6 ⊢ ((V ×_k V) ×_k V) ∈ V
14	7	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
15	13, 14	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
16		imakexg 4300	. . . . 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 ∧ SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V) → ((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V)
17	15, 16	mpan 651	. . . 4 ⊢ ( SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A) ∈ V → ((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V)
18	11, 12, 17	3syl 18	. . 3 ⊢ (A ∈ V → ((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V)
19		uni1exg 4293	. . 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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V → ⋃₁((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V)
20		uni1exg 4293	. . 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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V → ⋃₁⋃₁((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V)
21	18, 19, 20	3syl 18	. 2 ⊢ (A ∈ V → ⋃₁⋃₁((((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 SI_k (((V ×_k (V ×_k V)) ∩ ∼ (( 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 𝒫₁𝒫₁A)) ∈ V)
22	1, 21	syl5eqel 2437	1 ⊢ (A ∈ V → SI A ∈ V)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∈ 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 SI csi 4721

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-br 4641 df-si 4729

This theorem is used by: siex 4754 imageexg 5801 qsexg 5983

W3C validator