coexg - New Foundations Explorer

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

Theorem coexg 4750

Description: The composition of two sets is a set. (Contributed by SF, 7-Jan-2015.)

**Assertion**
Ref	Expression
coexg	⊢ ((A ∈ V ∧ B ∈ W) → (A ∘ B) ∈ V)

**Proof of Theorem coexg**
Step	Hyp	Ref	Expression
1		dfco1 4749	. 2 ⊢ (A ∘ B) = ⋃₁⋃₁((((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 ((((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) ∘_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 𝒫₁𝒫₁B)))
2		vvex 4110	. . . . . . 7 ⊢ V ∈ V
3	2, 2	xpkex 4290	. . . . . 6 ⊢ (V ×_k V) ∈ V
4	3, 2	xpkex 4290	. . . . 5 ⊢ ((V ×_k V) ×_k V) ∈ V
5		setconslem5 4736	. . . . . 6 ⊢ ∼ (( 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	. . . . 5 ⊢ ^◡_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	. . . 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)) ∈ V
8	2, 3	xpkex 4290	. . . . . . 7 ⊢ (V ×_k (V ×_k V)) ∈ V
9	8, 5	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
10		pw1exg 4303	. . . . . . 7 ⊢ (A ∈ V → 𝒫₁A ∈ V)
11		pw1exg 4303	. . . . . . 7 ⊢ (𝒫₁A ∈ V → 𝒫₁𝒫₁A ∈ V)
12	10, 11	syl 15	. . . . . 6 ⊢ (A ∈ V → 𝒫₁𝒫₁A ∈ V)
13		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)
14	9, 12, 13	sylancr 644	. . . . 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)
15		pw1exg 4303	. . . . . . 7 ⊢ (B ∈ W → 𝒫₁B ∈ V)
16		pw1exg 4303	. . . . . . 7 ⊢ (𝒫₁B ∈ V → 𝒫₁𝒫₁B ∈ V)
17	15, 16	syl 15	. . . . . 6 ⊢ (B ∈ W → 𝒫₁𝒫₁B ∈ V)
18		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 ∧ 𝒫₁𝒫₁B ∈ 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 𝒫₁𝒫₁B) ∈ V)
19	9, 17, 18	sylancr 644	. . . . 5 ⊢ (B ∈ W → (((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 𝒫₁𝒫₁B) ∈ V)
20		cokexg 4310	. . . . 5 ⊢ (((((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)) ∩ ∼ (( 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 𝒫₁𝒫₁B) ∈ 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) ∘_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 𝒫₁𝒫₁B)) ∈ V)
21	14, 19, 20	syl2an 463	. . . 4 ⊢ ((A ∈ V ∧ B ∈ W) → ((((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) ∘_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 𝒫₁𝒫₁B)) ∈ V)
22		imakexg 4300	. . . 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)) ∈ 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) ∘_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 𝒫₁𝒫₁B)) ∈ 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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ V)
23	7, 21, 22	sylancr 644	. . 3 ⊢ ((A ∈ V ∧ B ∈ W) → ((((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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ V)
24		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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ 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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ V)
25		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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ 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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ V)
26	23, 24, 25	3syl 18	. 2 ⊢ ((A ∈ V ∧ B ∈ W) → ⋃₁⋃₁((((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 ((((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) ∘_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 𝒫₁𝒫₁B))) ∈ V)
27	1, 26	syl5eqel 2437	1 ⊢ ((A ∈ V ∧ B ∈ W) → (A ∘ B) ∈ V)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 358 ∈ 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 ∘ ccom 4722

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-co 4727

This theorem is used by: coex 4751 txpexg 5785 imageexg 5801 composevalg 5818 pprodexg 5838 fullfunexg 5860 enmap2lem3 6066 enmap1lem3 6072

W3C validator