dfproj12 - New Foundations Explorer

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

Theorem dfproj12 4577

Description: Express the first projection operator via the set construction functors. (Contributed by SF, 2-Jan-2015.)

**Assertion**
Ref	Expression
dfproj12	⊢ Proj1 A = (^◡_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 A)

Proof of Theorem dfproj12 Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-proj1 4568	. 2 ⊢ Proj1 A = {x ∣ Phi x ∈ A}
2		vex 2863	. . . . . . 7 ⊢ x ∈ V
3		vex 2863	. . . . . . 7 ⊢ y ∈ V
4	2, 3	opkelimagek 4273	. . . . . 6 ⊢ (⟪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))
5	3, 2	opkelcnvk 4251	. . . . . 6 ⊢ (⟪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))))
6		dfphi2 4570	. . . . . . 7 ⊢ 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)
7	6	eqeq2i 2363	. . . . . 6 ⊢ (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))
8	4, 5, 7	3bitr4ri 269	. . . . 5 ⊢ (y = Phi x ↔ ⟪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))))
9	8	rexbii 2640	. . . 4 ⊢ (∃y ∈ A y = Phi x ↔ ∃y ∈ A ⟪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))))
10		risset 2662	. . . 4 ⊢ ( Phi x ∈ A ↔ ∃y ∈ A y = Phi x)
11	2	elimak 4260	. . . 4 ⊢ (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 A) ↔ ∃y ∈ A ⟪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))))
12	9, 10, 11	3bitr4ri 269	. . 3 ⊢ (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 A) ↔ Phi x ∈ A)
13	12	eqabi 2465	. 2 ⊢ (^◡_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 A) = {x ∣ Phi x ∈ A}
14	1, 13	eqtr4i 2376	1 ⊢ Proj1 A = (^◡_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 A)

Colors of variables: wff setvar class

This proof depends on syntax axioms: = wceq 1642 ∈ wcel 1710 {cab 2339 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 ⟪copk 4058 1_cc1c 4135 𝒫₁cpw1 4136 ×_k cxpk 4175 ^◡_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184 I_k cidk 4185 Nn cnnc 4374 Phi cphi 4563 Proj1 cproj1 4564

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-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-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-opk 4059 df-1c 4137 df-pw1 4138 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-idk 4196 df-addc 4379 df-phi 4566 df-proj1 4568

This theorem is used by: proj1eq 4590 proj1exg 4592

W3C validator