cbcpcp - Mathbox for Frédéric Liné

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
Unicode version

Theorem cbcpcp 14504

Description: The canonical bijection between a cross product and a cartesian product (whose set of indices is composed of two different elements). Bourbaki E.II.33 .

**Hypotheses**
Ref	Expression
cbcpcp.1
cbcpcp.2
cbcpcp.3
cbcpcp.4
cbcpcp.5

**Assertion**
Ref	Expression
cbcpcp

Distinct variable groups:

**Proof of Theorem cbcpcp**
Step	Hyp	Ref	Expression
1		prex 3526	. . . . . . 7
2	1	a1i 8	. . . . . 6 $/\$
3	2	rgen2 2186	. . . . 5
4	3	a1i 8	. . . 4
5		cbcpcp.3	. . . . . 6
6	5	fnoprab2ga 14470	. . . . 5
7	6	a1i 8	. . . 4
8	4, 7	mpbid 212	. . 3
9	5	rngop 14484	. . . . 5
10	9	a1i 8	. . . 4
11		cbcpcp.1	. . . . . 6
12		cbcpcp.2	. . . . . 6
13		cbcpcp.4	. . . . . . 7
14		elisset 2299	. . . . . . 7
15	13, 14	ax-mp 7	. . . . . 6
16		cbcpcp.5	. . . . . . 7
17		elisset 2299	. . . . . . 7
18	16, 17	ax-mp 7	. . . . . 6
19	11, 12, 15, 18	repcpwti 14503	. . . . 5
20	19	eqcomd 1889	. . . 4
21	10, 20	eqtrd 1925	. . 3
22		elxp 4018	. . . . . . 7 $/\$ $/\$
23		elxp 4018	. . . . . . . . . . . . 13 $/\$ $/\$
24		prex 3526	. . . . . . . . . . . . . . . . . 18
25		opeq2 3159	. . . . . . . . . . . . . . . . . . . . . . . 24
26		preq1 3098	. . . . . . . . . . . . . . . . . . . . . . . 24
27	25, 26	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23
28		opeq2 3159	. . . . . . . . . . . . . . . . . . . . . . . 24
29		preq2 3099	. . . . . . . . . . . . . . . . . . . . . . . 24
30	28, 29	syl 12	. . . . . . . . . . . . . . . . . . . . . . 23
31	27, 30, 5	ovmpt2g 5016	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
32		df-opr 4886	. . . . . . . . . . . . . . . . . . . . . . 23
33		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
34		prex 3526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
35		opeq2 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
36		preq1 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
37	35, 36	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
38		opeq2 3159	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
39		preq2 3099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
40	38, 39	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
41	37, 40, 5	ovmpt2g 5016	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$
42		df-opr 4886	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
43		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
44		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
45		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
46		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
47		opex 3527	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
48	44, 45, 46, 47	preq12b 3154	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $\/$ $/\$
49		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
50		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
51	49, 50	opth2 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
52		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
53		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
54	52, 53	opth2 3546	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
55		opeq12 3160	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$
56	55	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
57	56	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
58	57	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
59	58	com3l 38	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
60	54, 59	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
61	60	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
62	51, 61	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
63	62	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
64	15	opth1 3531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
65		df-ne 2019	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
66		pm2.21 92	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
67	65, 66	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
68	67	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
69	64, 68	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
70	69	adantr 425	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
71	63, 70	jaoi 368	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $\/$ $/\$
72	48, 71	sylbi 216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
73	72	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
74	73	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
75		eqeq2 1893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
76	75	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
77	76	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
78	74, 77	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
79	43, 78	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
80	79	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
81	80	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
82	42, 81	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
83	41, 82	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
84	83	3exp 1066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	84	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
86	85	com12 14	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
87	34, 86	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
88	87	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
89		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
90	89	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
91	90	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92	91	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
93	88, 92	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
94	33, 93	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
95	94	ex 402	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
96	95	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
97	32, 96	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
98	31, 97	syl 12	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
99	98	3exp 1066	. . . . . . . . . . . . . . . . . . . 20 $/\$
100	99	imp 377	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
101	100	com3l 38	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
102	24, 101	ax-mp 7	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
103	102	a1i 8	. . . . . . . . . . . . . . . 16 $/\$ $/\$
104		fveq2 4681	. . . . . . . . . . . . . . . . . . . . 21
105	104	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . 20
106		eqeq2 1893	. . . . . . . . . . . . . . . . . . . 20
107	105, 106	imbi12d 688	. . . . . . . . . . . . . . . . . . 19
108	107	imbi2d 674	. . . . . . . . . . . . . . . . . 18
109	108	imbi2d 674	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
110	109	imbi2d 674	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
111	103, 110	mpbird 213	. . . . . . . . . . . . . . 15 $/\$ $/\$
112	111	imp 377	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
113	112	19.23aivv 1675	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
114	23, 113	sylbi 216	. . . . . . . . . . . 12 $/\$
115	114	com12 14	. . . . . . . . . . 11 $/\$
116	115	a1i 8	. . . . . . . . . 10 $/\$
117		fveq2 4681	. . . . . . . . . . . . . . 15
118	117	eqeq1d 1892	. . . . . . . . . . . . . 14
119		eqeq1 1890	. . . . . . . . . . . . . 14
120	118, 119	imbi12d 688	. . . . . . . . . . . . 13
121	120	imbi2d 674	. . . . . . . . . . . 12
122	121	imbi2d 674	. . . . . . . . . . 11
123	122	imbi2d 674	. . . . . . . . . 10 $/\$ $/\$
124	116, 123	mpbird 213	. . . . . . . . 9 $/\$
125	124	imp 377	. . . . . . . 8 $/\$ $/\$
126	125	19.23aivv 1675	. . . . . . 7 $/\$ $/\$
127	22, 126	sylbi 216	. . . . . 6
128	127	imp 377	. . . . 5 $/\$
129	128	com12 14	. . . 4 $/\$
130	129	r19.21aivv 2183	. . 3
131	8, 21, 130	3jca 1050	. 2 $/\$ $/\$
132		dff1o6 4853	. 2 $/\$ $/\$
133	131, 132	sylibr 217	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wex 1326

cab 1871

wne 2017

wral 2105

wrex 2106

cvv 2292

cif 2982

cpr 3045

cop 3046

cxp 3984

crn 3987

wfn 3993

wf1o 3997

cfv 3998 (class class class)co 4884

cmpt2 5005

cixp 5406

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-5 1302 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-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-if 2983 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-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt2 5007 df-1st 5020 df-2nd 5021 df-ixp 5407