dfphi2 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > dfphi2		Unicode 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 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 _k ∼ Nn _k _k

Proof of Theorem dfphi2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 3669	. . . . . . . . 9 Nn Nn 1_c 1_c
2	1	eqeq2d 2364	. . . . . . . 8 Nn Nn 1_c 1_c
3		iba 489	. . . . . . . 8 Nn 1_c 1_c $/\$ Nn
4		simpr 447	. . . . . . . . . . 11 $/\$ Nn Nn
5	4	con2i 112	. . . . . . . . . 10 Nn $/\$ Nn
6		biorf 394	. . . . . . . . . 10 $/\$ Nn 1_c $/\$ Nn $/\$ Nn $\/$ 1_c $/\$ Nn
7	5, 6	syl 15	. . . . . . . . 9 Nn 1_c $/\$ Nn $/\$ Nn $\/$ 1_c $/\$ Nn
8		orcom 376	. . . . . . . . 9 $/\$ Nn $\/$ 1_c $/\$ Nn 1_c $/\$ Nn $\/$ $/\$ Nn
9	7, 8	syl6bb 252	. . . . . . . 8 Nn 1_c $/\$ Nn 1_c $/\$ Nn $\/$ $/\$ Nn
10	2, 3, 9	3bitrd 270	. . . . . . 7 Nn Nn 1_c 1_c $/\$ Nn $\/$ $/\$ Nn
11		iffalse 3670	. . . . . . . . 9 Nn Nn 1_c
12	11	eqeq2d 2364	. . . . . . . 8 Nn Nn 1_c
13		iba 489	. . . . . . . 8 Nn $/\$ Nn
14		simpr 447	. . . . . . . . . 10 1_c $/\$ Nn Nn
15	14	con3i 127	. . . . . . . . 9 Nn 1_c $/\$ Nn
16		biorf 394	. . . . . . . . 9 1_c $/\$ Nn $/\$ Nn 1_c $/\$ Nn $\/$ $/\$ Nn
17	15, 16	syl 15	. . . . . . . 8 Nn $/\$ Nn 1_c $/\$ Nn $\/$ $/\$ Nn
18	12, 13, 17	3bitrd 270	. . . . . . 7 Nn Nn 1_c 1_c $/\$ Nn $\/$ $/\$ Nn
19	10, 18	pm2.61i 156	. . . . . 6 Nn 1_c 1_c $/\$ Nn $\/$ $/\$ Nn
20		equcom 1680	. . . . . . . 8
21		vex 2863	. . . . . . . . 9
22	21	elcompl 3226	. . . . . . . 8 ∼ Nn Nn
23	20, 22	anbi12i 678	. . . . . . 7 $/\$ ∼ Nn $/\$ Nn
24	23	orbi2i 505	. . . . . 6 1_c $/\$ Nn $\/$ $/\$ ∼ Nn 1_c $/\$ Nn $\/$ $/\$ Nn
25	19, 24	bitr4i 243	. . . . 5 Nn 1_c 1_c $/\$ Nn $\/$ $/\$ ∼ Nn
26		elun 3221	. . . . . 6 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 _k ∼ Nn _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 $\/$ _k ∼ Nn _k
27		elin 3220	. . . . . . . 8 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 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
28		vex 2863	. . . . . . . . . . 11
29	21, 28	opkelimagek 4273	. . . . . . . . . 10 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 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
30		dfaddc2 4382	. . . . . . . . . . 11 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
31	30	eqeq2i 2363	. . . . . . . . . 10 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
32	29, 31	bitr4i 243	. . . . . . . . 9 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 1_c
33	21, 28	opkelxpk 4249	. . . . . . . . . 10 Nn _k Nn $/\$
34	28, 33	mpbiran2 885	. . . . . . . . 9 Nn _k Nn
35	32, 34	anbi12i 678	. . . . . . . 8 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 1_c $/\$ Nn
36	27, 35	bitri 240	. . . . . . 7 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 1_c $/\$ Nn
37		elin 3220	. . . . . . . 8 _k ∼ Nn _k _k $/\$ ∼ Nn _k
38		opkelidkg 4275	. . . . . . . . . 10 $/\$ _k
39	21, 28, 38	mp2an 653	. . . . . . . . 9 _k
40	21, 28	opkelxpk 4249	. . . . . . . . . 10 ∼ Nn _k ∼ Nn $/\$
41	28, 40	mpbiran2 885	. . . . . . . . 9 ∼ Nn _k ∼ Nn
42	39, 41	anbi12i 678	. . . . . . . 8 _k $/\$ ∼ Nn _k $/\$ ∼ Nn
43	37, 42	bitri 240	. . . . . . 7 _k ∼ Nn _k $/\$ ∼ Nn
44	36, 43	orbi12i 507	. . . . . 6 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 $\/$ _k ∼ Nn _k 1_c $/\$ Nn $\/$ $/\$ ∼ Nn
45	26, 44	bitri 240	. . . . 5 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 _k ∼ Nn _k 1_c $/\$ Nn $\/$ $/\$ ∼ Nn
46	25, 45	bitr4i 243	. . . 4 Nn 1_c 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 _k ∼ Nn _k
47	46	rexbii 2640	. . 3 Nn 1_c 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 _k ∼ Nn _k
48		eqeq1 2359	. . . . 5 Nn 1_c Nn 1_c
49	48	rexbidv 2636	. . . 4 Nn 1_c Nn 1_c
50		df-phi 4566	. . . 4 Phi Nn 1_c
51	28, 49, 50	elab2 2989	. . 3 Phi Nn 1_c
52	28	elimak 4260	. . 3 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 _k ∼ Nn _k _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 _k ∼ Nn _k
53	47, 51, 52	3bitr4i 268	. 2 Phi 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 _k ∼ Nn _k _k
54	53	eqriv 2350	1 Phi 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 _k ∼ Nn _k _k

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176 $\/$ wo 357 $/\$ wa 358

wceq 1642

wcel 1710

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cun 3208

cin 3209

csymdif 3210

cif 3663

copk 4058 1_cc1c 4135

₁ cpw1 4136

_k cxpk 4175 Ins2_k cins2k 4177 Ins3_k cins3k 4178

_kcimak 4180 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184

_k cidk 4185 Nn cnnc 4374

cplc 4376 Phi cphi 4563

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 4079 ax-sn 4088

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 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 referenced by: phieq 4571 phiexg 4572 dfop2lem1 4574 dfop2 4576 dfproj12 4577 setconslem1 4732 setconslem2 4733 dfswap2 4742

W3C validator