prj1 - Mathbox for Frédéric Liné

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
Unicode version

Theorem prj1 14395

Description: Projection of the first elements of the pairs of a class

**Assertion**
Ref	Expression
prj1

Distinct variable group:

**Proof of Theorem prj1**
Step	Hyp	Ref	Expression
1		df-rel 4001	. . . . . . . . . 10
2		ssel 2615	. . . . . . . . . . 11
3		elxp6 5041	. . . . . . . . . . . . 13 $/\$ $/\$
4		eleq1 1957	. . . . . . . . . . . . . . . . 17
5		fo1st 5032	. . . . . . . . . . . . . . . . . . . . . 22
6		fofun 4618	. . . . . . . . . . . . . . . . . . . . . 22
7	5, 6	ax-mp 7	. . . . . . . . . . . . . . . . . . . . 21
8		funres 4459	. . . . . . . . . . . . . . . . . . . . 21
9	7, 8	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20
10		visset 2295	. . . . . . . . . . . . . . . . . . . . 21
11	10	funbrfv 4709	. . . . . . . . . . . . . . . . . . . 20
12	9, 11	ax-mp 7	. . . . . . . . . . . . . . . . . . 19
13		fvres 4691	. . . . . . . . . . . . . . . . . . . . 21
14		eqtr2 1905	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
15	14	ex 402	. . . . . . . . . . . . . . . . . . . . . 22
16		opeq1 3158	. . . . . . . . . . . . . . . . . . . . . . . . 25
17	16	eleq1d 1963	. . . . . . . . . . . . . . . . . . . . . . . 24
18	17	biimpd 170	. . . . . . . . . . . . . . . . . . . . . . 23
19	18	a1d 15	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
20	15, 19	syl6 25	. . . . . . . . . . . . . . . . . . . . 21 $/\$
21	13, 20	syl 12	. . . . . . . . . . . . . . . . . . . 20 $/\$
22	21	com4l 43	. . . . . . . . . . . . . . . . . . 19 $/\$
23	12, 22	syl 12	. . . . . . . . . . . . . . . . . 18 $/\$
24	23	com13 37	. . . . . . . . . . . . . . . . 17 $/\$
25	4, 24	syl6bi 231	. . . . . . . . . . . . . . . 16 $/\$
26	25	com23 36	. . . . . . . . . . . . . . 15 $/\$
27	26	imp 377	. . . . . . . . . . . . . 14 $/\$ $/\$
28	27	com24 41	. . . . . . . . . . . . 13 $/\$ $/\$
29	3, 28	sylbi 216	. . . . . . . . . . . 12
30	29	pm2.43i 78	. . . . . . . . . . 11
31	2, 30	syl6 25	. . . . . . . . . 10
32	1, 31	sylbi 216	. . . . . . . . 9
33	32	com14 42	. . . . . . . 8
34	33	pm2.43i 78	. . . . . . 7
35		fvex 4689	. . . . . . . 8
36		opeq2 3159	. . . . . . . . 9
37	36	eleq1d 1963	. . . . . . . 8
38	35, 37	cla4ev 2371	. . . . . . 7
39	34, 38	syl8 27	. . . . . 6
40	39	r19.23aiv 2211	. . . . 5
41	40	com12 14	. . . 4
42		df-opr 4886	. . . . . . . . 9
43		visset 2295	. . . . . . . . . . . 12
44	43	opelxp 4036	. . . . . . . . . . 11 $/\$
45	44, 10, 43	mpbir2an 800	. . . . . . . . . 10
46		fvres 4691	. . . . . . . . . 10
47	45, 46	ax-mp 7	. . . . . . . . 9
48	10	op1st 5026	. . . . . . . . 9
49	42, 47, 48	3eqtri 1912	. . . . . . . 8
50		ssv 2636	. . . . . . . . . 10
51		fofn 4619	. . . . . . . . . . . 12
52	5, 51	ax-mp 7	. . . . . . . . . . 11
53		fnssresb 4525	. . . . . . . . . . 11
54	52, 53	ax-mp 7	. . . . . . . . . 10
55	50, 54	mpbir 207	. . . . . . . . 9
56	10	fnotoprb 4916	. . . . . . . . 9 $/\$ $/\$
57	55, 10, 43, 56	mp3an 1191	. . . . . . . 8
58	49, 57	mpbi 206	. . . . . . 7
59		df-br 3339	. . . . . . 7
60	58, 59	mpbir 207	. . . . . 6
61		breq1 3341	. . . . . . 7
62	61	rcla4ev 2381	. . . . . 6 $/\$
63	60, 62	mpan2 760	. . . . 5
64	63	19.23aiv 1674	. . . 4
65	41, 64	impbid1 575	. . 3
66	10	elima 4270	. . 3
67		opeq1 3158	. . . . . 6
68	67	eleq1d 1963	. . . . 5
69	68	exbidv 1657	. . . 4
70	10, 69	elab 2403	. . 3
71	65, 66, 70	3bitr4g 614	. 2
72	71	eqrdv 1882	1

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240

wceq 1298

wcel 1300

wex 1326

cab 1871

wrex 2106

cvv 2292

wss 2593

cop 3046 class class class wbr 3338

cxp 3984

cres 3988

cima 3989

wrel 3991

wfun 3992

wfn 3993

wfo 3996

cfv 3998 (class class class)co 4884

c1st 5018

c2nd 5019

This theorem is referenced by: prj1b 14397

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-id 3586 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-fo 4012 df-fv 4014 df-opr 4886 df-1st 5020 df-2nd 5021