dfop2lem1 - New Foundations Explorer

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

Theorem dfop2lem1 4573

Description: Lemma for dfop2 4575 and dfproj22 4577. (Contributed by SF, 2-Jan-2015.)

**Assertion**
Ref	Expression
dfop2lem1	⊢ (⟪x, y⟫ ∈ ∼ (( 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) ↔ y = ( Phi x ∪ {0_c}))

Distinct variable group: x,y

Proof of Theorem dfop2lem1 Dummy variables z t are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opkex 4113	. . . . 5 ⊢ ⟪x, y⟫ ∈ V
2	1	elimak 4259	. . . 4 ⊢ (⟪x, y⟫ ∈ (( 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) ↔ ∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪x, y⟫⟫ ∈ ( 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))))
3		elpw121c 4148	. . . . . . . 8 ⊢ (t ∈ ℘₁℘₁1_c ↔ ∃z t = {{{z}}})
4	3	anbi1i 676	. . . . . . 7 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
5		19.41v 1901	. . . . . . 7 ⊢ (∃z(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ (∃z t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
6	4, 5	bitr4i 243	. . . . . 6 ⊢ ((t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ ∃z(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
7	6	exbii 1582	. . . . 5 ⊢ (∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
8		df-rex 2620	. . . . 5 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪x, y⟫⟫ ∈ ( 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))) ↔ ∃t(t ∈ ℘₁℘₁1_c ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
9		excom 1741	. . . . 5 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ ∃t∃z(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
10	7, 8, 9	3bitr4i 268	. . . 4 ⊢ (∃t ∈ ℘₁ ℘₁1_c⟪t, ⟪x, y⟫⟫ ∈ ( 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))) ↔ ∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))))
11		snex 4111	. . . . . . 7 ⊢ {{{z}}} ∈ V
12		opkeq1 4059	. . . . . . . 8 ⊢ (t = {{{z}}} → ⟪t, ⟪x, y⟫⟫ = ⟪{{{z}}}, ⟪x, y⟫⟫)
13	12	eleq1d 2419	. . . . . . 7 ⊢ (t = {{{z}}} → (⟪t, ⟪x, y⟫⟫ ∈ ( 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))) ↔ ⟪{{{z}}}, ⟪x, y⟫⟫ ∈ ( 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)))))
14	11, 13	ceqsexv 2894	. . . . . 6 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ ⟪{{{z}}}, ⟪x, y⟫⟫ ∈ ( 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))))
15		elsymdif 3223	. . . . . 6 ⊢ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ ( 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))) ↔ ¬ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪x, y⟫⟫ ∈ 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))))
16		snex 4111	. . . . . . . . . 10 ⊢ {z} ∈ V
17		vex 2862	. . . . . . . . . 10 ⊢ x ∈ V
18		vex 2862	. . . . . . . . . 10 ⊢ y ∈ V
19	16, 17, 18	otkelins2k 4255	. . . . . . . . 9 ⊢ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ Ins2_k S_k ↔ ⟪{z}, y⟫ ∈ S_k )
20		vex 2862	. . . . . . . . . 10 ⊢ z ∈ V
21	20, 18	elssetk 4270	. . . . . . . . 9 ⊢ (⟪{z}, y⟫ ∈ S_k ↔ z ∈ y)
22	19, 21	bitri 240	. . . . . . . 8 ⊢ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ Ins2_k S_k ↔ z ∈ y)
23	16, 17, 18	otkelins3k 4256	. . . . . . . . 9 ⊢ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ 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)) ↔ ⟪{z}, x⟫ ∈ ((^◡_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)))
24		elun 3220	. . . . . . . . 9 ⊢ (⟪{z}, x⟫ ∈ ((^◡_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)) ↔ (⟪{z}, x⟫ ∈ (^◡_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 ) ∨ ⟪{z}, x⟫ ∈ ({{0_c}} ×_k V)))
25		ancom 437	. . . . . . . . . . . . . 14 ⊢ ((⟪{z}, y⟫ ∈ S_k ∧ ⟪y, x⟫ ∈ ^◡_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)))) ↔ (⟪y, x⟫ ∈ ^◡_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))) ∧ ⟪{z}, y⟫ ∈ S_k ))
26	17, 18	opkelimagek 4272	. . . . . . . . . . . . . . . 16 ⊢ (⟪x, y⟫ ∈ Image_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))) ↔ y = (((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 x))
27	18, 17	opkelcnvk 4250	. . . . . . . . . . . . . . . 16 ⊢ (⟪y, x⟫ ∈ ^◡_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))) ↔ ⟪x, y⟫ ∈ Image_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))))
28		dfphi2 4569	. . . . . . . . . . . . . . . . 17 ⊢ Phi x = (((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 x)
29	28	eqeq2i 2363	. . . . . . . . . . . . . . . 16 ⊢ (y = Phi x ↔ y = (((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 x))
30	26, 27, 29	3bitr4i 268	. . . . . . . . . . . . . . 15 ⊢ (⟪y, x⟫ ∈ ^◡_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))) ↔ y = Phi x)
31	30, 21	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ ((⟪y, x⟫ ∈ ^◡_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))) ∧ ⟪{z}, y⟫ ∈ S_k ) ↔ (y = Phi x ∧ z ∈ y))
32	25, 31	bitri 240	. . . . . . . . . . . . 13 ⊢ ((⟪{z}, y⟫ ∈ S_k ∧ ⟪y, x⟫ ∈ ^◡_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)))) ↔ (y = Phi x ∧ z ∈ y))
33	32	exbii 1582	. . . . . . . . . . . 12 ⊢ (∃y(⟪{z}, y⟫ ∈ S_k ∧ ⟪y, x⟫ ∈ ^◡_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)))) ↔ ∃y(y = Phi x ∧ z ∈ y))
34	16, 17	opkelcok 4262	. . . . . . . . . . . 12 ⊢ (⟪{z}, x⟫ ∈ (^◡_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 ) ↔ ∃y(⟪{z}, y⟫ ∈ S_k ∧ ⟪y, x⟫ ∈ ^◡_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)))))
35	17	phiex 4572	. . . . . . . . . . . . 13 ⊢ Phi x ∈ V
36	35	clel3 2977	. . . . . . . . . . . 12 ⊢ (z ∈ Phi x ↔ ∃y(y = Phi x ∧ z ∈ y))
37	33, 34, 36	3bitr4i 268	. . . . . . . . . . 11 ⊢ (⟪{z}, x⟫ ∈ (^◡_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 ) ↔ z ∈ Phi x)
38	16, 17	opkelxpk 4248	. . . . . . . . . . . . 13 ⊢ (⟪{z}, x⟫ ∈ ({{0_c}} ×_k V) ↔ ({z} ∈ {{0_c}} ∧ x ∈ V))
39	17, 38	mpbiran2 885	. . . . . . . . . . . 12 ⊢ (⟪{z}, x⟫ ∈ ({{0_c}} ×_k V) ↔ {z} ∈ {{0_c}})
40	20	sneqb 3876	. . . . . . . . . . . . 13 ⊢ ({z} = {0_c} ↔ z = 0_c)
41	16	elsnc 3756	. . . . . . . . . . . . 13 ⊢ ({z} ∈ {{0_c}} ↔ {z} = {0_c})
42	20	elsnc 3756	. . . . . . . . . . . . 13 ⊢ (z ∈ {0_c} ↔ z = 0_c)
43	40, 41, 42	3bitr4ri 269	. . . . . . . . . . . 12 ⊢ (z ∈ {0_c} ↔ {z} ∈ {{0_c}})
44	39, 43	bitr4i 243	. . . . . . . . . . 11 ⊢ (⟪{z}, x⟫ ∈ ({{0_c}} ×_k V) ↔ z ∈ {0_c})
45	37, 44	orbi12i 507	. . . . . . . . . 10 ⊢ ((⟪{z}, x⟫ ∈ (^◡_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 ) ∨ ⟪{z}, x⟫ ∈ ({{0_c}} ×_k V)) ↔ (z ∈ Phi x ∨ z ∈ {0_c}))
46		elun 3220	. . . . . . . . . 10 ⊢ (z ∈ ( Phi x ∪ {0_c}) ↔ (z ∈ Phi x ∨ z ∈ {0_c}))
47	45, 46	bitr4i 243	. . . . . . . . 9 ⊢ ((⟪{z}, x⟫ ∈ (^◡_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 ) ∨ ⟪{z}, x⟫ ∈ ({{0_c}} ×_k V)) ↔ z ∈ ( Phi x ∪ {0_c}))
48	23, 24, 47	3bitri 262	. . . . . . . 8 ⊢ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ 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)) ↔ z ∈ ( Phi x ∪ {0_c}))
49	22, 48	bibi12i 306	. . . . . . 7 ⊢ ((⟪{{{z}}}, ⟪x, y⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪x, y⟫⟫ ∈ 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))) ↔ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
50	49	notbii 287	. . . . . 6 ⊢ (¬ (⟪{{{z}}}, ⟪x, y⟫⟫ ∈ Ins2_k S_k ↔ ⟪{{{z}}}, ⟪x, y⟫⟫ ∈ 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))) ↔ ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
51	14, 15, 50	3bitri 262	. . . . 5 ⊢ (∃t(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
52	51	exbii 1582	. . . 4 ⊢ (∃z∃t(t = {{{z}}} ∧ ⟪t, ⟪x, y⟫⟫ ∈ ( 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)))) ↔ ∃z ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
53	2, 10, 52	3bitri 262	. . 3 ⊢ (⟪x, y⟫ ∈ (( 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) ↔ ∃z ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
54	53	notbii 287	. 2 ⊢ (¬ ⟪x, y⟫ ∈ (( 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) ↔ ¬ ∃z ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
55	1	elcompl 3225	. 2 ⊢ (⟪x, y⟫ ∈ ∼ (( 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) ↔ ¬ ⟪x, y⟫ ∈ (( 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))
56		dfcleq 2347	. . 3 ⊢ (y = ( Phi x ∪ {0_c}) ↔ ∀z(z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
57		alex 1572	. . 3 ⊢ (∀z(z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})) ↔ ¬ ∃z ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
58	56, 57	bitri 240	. 2 ⊢ (y = ( Phi x ∪ {0_c}) ↔ ¬ ∃z ¬ (z ∈ y ↔ z ∈ ( Phi x ∪ {0_c})))
59	54, 55, 58	3bitr4i 268	1 ⊢ (⟪x, y⟫ ∈ ∼ (( 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) ↔ y = ( Phi x ∪ {0_c}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 176 ∨ wo 357 ∧ wa 358 ∀wal 1540 ∃wex 1541 = wceq 1642 ∈ wcel 1710 ∃wrex 2615 Vcvv 2859 ∼ ccompl 3205 ∖ cdif 3206 ∪ cun 3207 ∩ cin 3208 ⊕ csymdif 3209 {csn 3737 ⟪copk 4057 1_cc1c 4134 ℘₁cpw1 4135 ×_k cxpk 4174 ^◡_kccnvk 4175 Ins2_k cins2k 4176 Ins3_k cins3k 4177 “_k cimak 4179 ∘_k ccomk 4180 SI_k csik 4181 Image_kcimagek 4182 S_k cssetk 4183 I_k cidk 4184 Nn cnnc 4373 0_cc0c 4374 Phi cphi 4562

This theorem was proved from 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 4078 ax-xp 4079 ax-cnv 4080 ax-1c 4081 ax-sset 4082 ax-si 4083 ax-ins2 4084 ax-ins3 4085 ax-typlower 4086 ax-sn 4087

This theorem 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 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-idk 4195 df-addc 4378 df-nnc 4379 df-phi 4565

This theorem is referenced by: dfop2lem2 4574 dfproj22 4577 dfswap2 4741

W3C validator