dfphi2 - New Foundations Explorer

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

Theorem dfphi2 4570

Description: Express the phi operator in terms of the Kuratowski set construction functions. (Contributed by SF, 3-Feb-2015.)

**Assertion**
Ref	Expression
dfphi2	⊢ Phi A = (((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 dfphi2 Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 3669	. . . . . . . . 9 ⊢ (y ∈ Nn → if(y ∈ Nn , (y +_c 1_c), y) = (y +_c 1_c))
2	1	eqeq2d 2364	. . . . . . . 8 ⊢ (y ∈ Nn → (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ x = (y +_c 1_c)))
3		iba 489	. . . . . . . 8 ⊢ (y ∈ Nn → (x = (y +_c 1_c) ↔ (x = (y +_c 1_c) ∧ y ∈ Nn )))
4		simpr 447	. . . . . . . . . . 11 ⊢ ((x = y ∧ ¬ y ∈ Nn ) → ¬ y ∈ Nn )
5	4	con2i 112	. . . . . . . . . 10 ⊢ (y ∈ Nn → ¬ (x = y ∧ ¬ y ∈ Nn ))
6		biorf 394	. . . . . . . . . 10 ⊢ (¬ (x = y ∧ ¬ y ∈ Nn ) → ((x = (y +_c 1_c) ∧ y ∈ Nn ) ↔ ((x = y ∧ ¬ y ∈ Nn ) ∨ (x = (y +_c 1_c) ∧ y ∈ Nn ))))
7	5, 6	syl 15	. . . . . . . . 9 ⊢ (y ∈ Nn → ((x = (y +_c 1_c) ∧ y ∈ Nn ) ↔ ((x = y ∧ ¬ y ∈ Nn ) ∨ (x = (y +_c 1_c) ∧ y ∈ Nn ))))
8		orcom 376	. . . . . . . . 9 ⊢ (((x = y ∧ ¬ y ∈ Nn ) ∨ (x = (y +_c 1_c) ∧ y ∈ Nn )) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn )))
9	7, 8	syl6bb 252	. . . . . . . 8 ⊢ (y ∈ Nn → ((x = (y +_c 1_c) ∧ y ∈ Nn ) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn ))))
10	2, 3, 9	3bitrd 270	. . . . . . 7 ⊢ (y ∈ Nn → (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn ))))
11		iffalse 3670	. . . . . . . . 9 ⊢ (¬ y ∈ Nn → if(y ∈ Nn , (y +_c 1_c), y) = y)
12	11	eqeq2d 2364	. . . . . . . 8 ⊢ (¬ y ∈ Nn → (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ x = y))
13		iba 489	. . . . . . . 8 ⊢ (¬ y ∈ Nn → (x = y ↔ (x = y ∧ ¬ y ∈ Nn )))
14		simpr 447	. . . . . . . . . 10 ⊢ ((x = (y +_c 1_c) ∧ y ∈ Nn ) → y ∈ Nn )
15	14	con3i 127	. . . . . . . . 9 ⊢ (¬ y ∈ Nn → ¬ (x = (y +_c 1_c) ∧ y ∈ Nn ))
16		biorf 394	. . . . . . . . 9 ⊢ (¬ (x = (y +_c 1_c) ∧ y ∈ Nn ) → ((x = y ∧ ¬ y ∈ Nn ) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn ))))
17	15, 16	syl 15	. . . . . . . 8 ⊢ (¬ y ∈ Nn → ((x = y ∧ ¬ y ∈ Nn ) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn ))))
18	12, 13, 17	3bitrd 270	. . . . . . 7 ⊢ (¬ y ∈ Nn → (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn ))))
19	10, 18	pm2.61i 156	. . . . . 6 ⊢ (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn )))
20		equcom 1680	. . . . . . . 8 ⊢ (y = x ↔ x = y)
21		vex 2863	. . . . . . . . 9 ⊢ y ∈ V
22	21	elcompl 3226	. . . . . . . 8 ⊢ (y ∈ ∼ Nn ↔ ¬ y ∈ Nn )
23	20, 22	anbi12i 678	. . . . . . 7 ⊢ ((y = x ∧ y ∈ ∼ Nn ) ↔ (x = y ∧ ¬ y ∈ Nn ))
24	23	orbi2i 505	. . . . . 6 ⊢ (((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (y = x ∧ y ∈ ∼ Nn )) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (x = y ∧ ¬ y ∈ Nn )))
25	19, 24	bitr4i 243	. . . . 5 ⊢ (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (y = x ∧ y ∈ ∼ Nn )))
26		elun 3221	. . . . . 6 ⊢ (⟪y, 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))) ↔ (⟪y, 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)) ∨ ⟪y, x⟫ ∈ ( I_k ∩ ( ∼ Nn ×_k V))))
27		elin 3220	. . . . . . . 8 ⊢ (⟪y, 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)) ↔ (⟪y, 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) ∧ ⟪y, x⟫ ∈ ( Nn ×_k V)))
28		vex 2863	. . . . . . . . . . 11 ⊢ x ∈ V
29	21, 28	opkelimagek 4273	. . . . . . . . . 10 ⊢ (⟪y, 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) ↔ x = ((( 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) “_k y))
30		dfaddc2 4382	. . . . . . . . . . 11 ⊢ (y +_c 1_c) = ((( 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) “_k y)
31	30	eqeq2i 2363	. . . . . . . . . 10 ⊢ (x = (y +_c 1_c) ↔ x = ((( 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) “_k y))
32	29, 31	bitr4i 243	. . . . . . . . 9 ⊢ (⟪y, 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) ↔ x = (y +_c 1_c))
33	21, 28	opkelxpk 4249	. . . . . . . . . 10 ⊢ (⟪y, x⟫ ∈ ( Nn ×_k V) ↔ (y ∈ Nn ∧ x ∈ V))
34	28, 33	mpbiran2 885	. . . . . . . . 9 ⊢ (⟪y, x⟫ ∈ ( Nn ×_k V) ↔ y ∈ Nn )
35	32, 34	anbi12i 678	. . . . . . . 8 ⊢ ((⟪y, 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) ∧ ⟪y, x⟫ ∈ ( Nn ×_k V)) ↔ (x = (y +_c 1_c) ∧ y ∈ Nn ))
36	27, 35	bitri 240	. . . . . . 7 ⊢ (⟪y, 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)) ↔ (x = (y +_c 1_c) ∧ y ∈ Nn ))
37		elin 3220	. . . . . . . 8 ⊢ (⟪y, x⟫ ∈ ( I_k ∩ ( ∼ Nn ×_k V)) ↔ (⟪y, x⟫ ∈ I_k ∧ ⟪y, x⟫ ∈ ( ∼ Nn ×_k V)))
38		opkelidkg 4275	. . . . . . . . . 10 ⊢ ((y ∈ V ∧ x ∈ V) → (⟪y, x⟫ ∈ I_k ↔ y = x))
39	21, 28, 38	mp2an 653	. . . . . . . . 9 ⊢ (⟪y, x⟫ ∈ I_k ↔ y = x)
40	21, 28	opkelxpk 4249	. . . . . . . . . 10 ⊢ (⟪y, x⟫ ∈ ( ∼ Nn ×_k V) ↔ (y ∈ ∼ Nn ∧ x ∈ V))
41	28, 40	mpbiran2 885	. . . . . . . . 9 ⊢ (⟪y, x⟫ ∈ ( ∼ Nn ×_k V) ↔ y ∈ ∼ Nn )
42	39, 41	anbi12i 678	. . . . . . . 8 ⊢ ((⟪y, x⟫ ∈ I_k ∧ ⟪y, x⟫ ∈ ( ∼ Nn ×_k V)) ↔ (y = x ∧ y ∈ ∼ Nn ))
43	37, 42	bitri 240	. . . . . . 7 ⊢ (⟪y, x⟫ ∈ ( I_k ∩ ( ∼ Nn ×_k V)) ↔ (y = x ∧ y ∈ ∼ Nn ))
44	36, 43	orbi12i 507	. . . . . 6 ⊢ ((⟪y, 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)) ∨ ⟪y, x⟫ ∈ ( I_k ∩ ( ∼ Nn ×_k V))) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (y = x ∧ y ∈ ∼ Nn )))
45	26, 44	bitri 240	. . . . 5 ⊢ (⟪y, 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))) ↔ ((x = (y +_c 1_c) ∧ y ∈ Nn ) ∨ (y = x ∧ y ∈ ∼ Nn )))
46	25, 45	bitr4i 243	. . . 4 ⊢ (x = if(y ∈ Nn , (y +_c 1_c), y) ↔ ⟪y, 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))))
47	46	rexbii 2640	. . 3 ⊢ (∃y ∈ A x = if(y ∈ Nn , (y +_c 1_c), y) ↔ ∃y ∈ A ⟪y, 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))))
48		eqeq1 2359	. . . . 5 ⊢ (z = x → (z = if(y ∈ Nn , (y +_c 1_c), y) ↔ x = if(y ∈ Nn , (y +_c 1_c), y)))
49	48	rexbidv 2636	. . . 4 ⊢ (z = x → (∃y ∈ A z = if(y ∈ Nn , (y +_c 1_c), y) ↔ ∃y ∈ A x = if(y ∈ Nn , (y +_c 1_c), y)))
50		df-phi 4566	. . . 4 ⊢ Phi A = {z ∣ ∃y ∈ A z = if(y ∈ Nn , (y +_c 1_c), y)}
51	28, 49, 50	elab2 2989	. . 3 ⊢ (x ∈ Phi A ↔ ∃y ∈ A x = if(y ∈ Nn , (y +_c 1_c), y))
52	28	elimak 4260	. . 3 ⊢ (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 A) ↔ ∃y ∈ A ⟪y, 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))))
53	47, 51, 52	3bitr4i 268	. 2 ⊢ (x ∈ Phi A ↔ 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 A))
54	53	eqriv 2350	1 ⊢ Phi A = (((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: ¬ wn 3 ↔ wb 176 ∨ wo 357 ∧ wa 358 = wceq 1642 ∈ wcel 1710 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 ifcif 3663 ⟪copk 4058 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 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 +_c cplc 4376 Phi cphi 4563

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

This theorem is used by: phieq 4571 phiexg 4572 dfop2lem1 4574 dfop2 4576 dfproj12 4577 setconslem1 4732 setconslem2 4733 dfswap2 4742

W3C validator