cnref1o - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > cnref1o		Unicode version

Theorem cnref1o 8814

Description: There is a natural one-to-one mapping from

, where we map

. In our construction of the complex numbers, this is in fact our definition of

(see df-c 7049), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.)

**Hypothesis**
Ref	Expression
cnref1o.1

**Assertion**
Ref	Expression
cnref1o

Distinct variable group:

Allowed substitution hints:

(

)

Proof of Theorem cnref1o Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 107	. . . . . . . 8 $/\$
2	1	recnd 7209	. . . . . . 7 $/\$
3		ax-icn 7133	. . . . . . . . 9
4	3	a1i 9	. . . . . . . 8 $/\$
5		simpr 108	. . . . . . . . 9 $/\$
6	5	recnd 7209	. . . . . . . 8 $/\$
7	4, 6	mulcld 7201	. . . . . . 7 $/\$
8	2, 7	addcld 7200	. . . . . 6 $/\$
9	8	rgen2a 2418	. . . . 5
10		cnref1o.1	. . . . . 6
11	10	fnmpt2 5859	. . . . 5
12	9, 11	ax-mp 7	. . . 4
13		1st2nd2 5832	. . . . . . . . 9
14	13	fveq2d 5213	. . . . . . . 8
15		df-ov 5546	. . . . . . . 8
16	14, 15	syl6eqr 2132	. . . . . . 7
17		xp1st 5823	. . . . . . . 8
18		xp2nd 5824	. . . . . . . 8
19	17	recnd 7209	. . . . . . . . 9
20	3	a1i 9	. . . . . . . . . 10
21	18	recnd 7209	. . . . . . . . . 10
22	20, 21	mulcld 7201	. . . . . . . . 9
23	19, 22	addcld 7200	. . . . . . . 8
24		oveq1 5550	. . . . . . . . 9
25		oveq2 5551	. . . . . . . . . 10
26	25	oveq2d 5559	. . . . . . . . 9
27	24, 26, 10	ovmpt2g 5666	. . . . . . . 8 $/\$ $/\$
28	17, 18, 23, 27	syl3anc 1170	. . . . . . 7
29	16, 28	eqtrd 2114	. . . . . 6
30	29, 23	eqeltrd 2156	. . . . 5
31	30	rgen 2417	. . . 4
32		ffnfv 5355	. . . 4 $/\$
33	12, 31, 32	mpbir2an 884	. . 3
34	17, 18	jca 300	. . . . . . 7 $/\$
35		xp1st 5823	. . . . . . . 8
36		xp2nd 5824	. . . . . . . 8
37	35, 36	jca 300	. . . . . . 7 $/\$
38		cru 7769	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
39	34, 37, 38	syl2an 283	. . . . . 6 $/\$ $/\$
40		fveq2 5209	. . . . . . . . 9
41		fveq2 5209	. . . . . . . . . 10
42		fveq2 5209	. . . . . . . . . . 11
43	42	oveq2d 5559	. . . . . . . . . 10
44	41, 43	oveq12d 5561	. . . . . . . . 9
45	40, 44	eqeq12d 2096	. . . . . . . 8
46	45, 29	vtoclga 2665	. . . . . . 7
47	29, 46	eqeqan12d 2097	. . . . . 6 $/\$
48		1st2nd2 5832	. . . . . . . 8
49	13, 48	eqeqan12d 2097	. . . . . . 7 $/\$
50		vex 2605	. . . . . . . . 9
51		1stexg 5825	. . . . . . . . 9
52	50, 51	ax-mp 7	. . . . . . . 8
53		2ndexg 5826	. . . . . . . . 9
54	50, 53	ax-mp 7	. . . . . . . 8
55	52, 54	opth 4000	. . . . . . 7 $/\$
56	49, 55	syl6bb 194	. . . . . 6 $/\$ $/\$
57	39, 47, 56	3bitr4d 218	. . . . 5 $/\$
58	57	biimpd 142	. . . 4 $/\$
59	58	rgen2a 2418	. . 3
60		dff13 5439	. . 3 $/\$
61	33, 59, 60	mpbir2an 884	. 2
62		cnre 7177	. . . . . 6
63		simpl 107	. . . . . . . . 9 $/\$
64		simpr 108	. . . . . . . . 9 $/\$
65	63	recnd 7209	. . . . . . . . . 10 $/\$
66	3	a1i 9	. . . . . . . . . . 11 $/\$
67	64	recnd 7209	. . . . . . . . . . 11 $/\$
68	66, 67	mulcld 7201	. . . . . . . . . 10 $/\$
69	65, 68	addcld 7200	. . . . . . . . 9 $/\$
70		oveq1 5550	. . . . . . . . . 10
71		oveq2 5551	. . . . . . . . . . 11
72	71	oveq2d 5559	. . . . . . . . . 10
73	70, 72, 10	ovmpt2g 5666	. . . . . . . . 9 $/\$ $/\$
74	63, 64, 69, 73	syl3anc 1170	. . . . . . . 8 $/\$
75	74	eqeq2d 2093	. . . . . . 7 $/\$
76	75	2rexbiia 2383	. . . . . 6
77	62, 76	sylibr 132	. . . . 5
78		fveq2 5209	. . . . . . . 8
79		df-ov 5546	. . . . . . . 8
80	78, 79	syl6eqr 2132	. . . . . . 7
81	80	eqeq2d 2093	. . . . . 6
82	81	rexxp 4508	. . . . 5
83	77, 82	sylibr 132	. . . 4
84	83	rgen 2417	. . 3
85		dffo3 5346	. . 3 $/\$
86	33, 84, 85	mpbir2an 884	. 2
87		df-f1o 4939	. 2 $/\$
88	61, 86, 87	mpbir2an 884	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 102

wb 103

wceq 1285

wcel 1434

wral 2349

wrex 2350

cvv 2602

cop 3409

cxp 4369

wfn 4927

wf 4928

wf1 4929

wfo 4930

wf1o 4931

cfv 4932 (class class class)co 5543

cmpt2 5545

c1st 5796

c2nd 5797

cc 7041

cr 7042

ci 7045

caddc 7046

cmul 7048

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3904 ax-pow 3956 ax-pr 3972 ax-un 4196 ax-setind 4288 ax-cnex 7129 ax-resscn 7130 ax-1cn 7131 ax-1re 7132 ax-icn 7133 ax-addcl 7134 ax-addrcl 7135 ax-mulcl 7136 ax-mulrcl 7137 ax-addcom 7138 ax-mulcom 7139 ax-addass 7140 ax-mulass 7141 ax-distr 7142 ax-i2m1 7143 ax-0lt1 7144 ax-1rid 7145 ax-0id 7146 ax-rnegex 7147 ax-precex 7148 ax-cnre 7149 ax-pre-ltirr 7150 ax-pre-lttrn 7152 ax-pre-apti 7153 ax-pre-ltadd 7154 ax-pre-mulgt0 7155

This theorem depends on definitions: df-bi 115 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-reu 2356 df-rab 2358 df-v 2604 df-sbc 2817 df-csb 2910 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3392 df-sn 3412 df-pr 3413 df-op 3415 df-uni 3610 df-iun 3688 df-br 3794 df-opab 3848 df-mpt 3849 df-id 4056 df-xp 4377 df-rel 4378 df-cnv 4379 df-co 4380 df-dm 4381 df-rn 4382 df-res 4383 df-ima 4384 df-iota 4897 df-fun 4934 df-fn 4935 df-f 4936 df-f1 4937 df-fo 4938 df-f1o 4939 df-fv 4940 df-riota 5499 df-ov 5546 df-oprab 5547 df-mpt2 5548 df-1st 5798 df-2nd 5799 df-pnf 7217 df-mnf 7218 df-ltxr 7220 df-sub 7348 df-neg 7349 df-reap 7742

This theorem is referenced by: cnrecnv 9935

W3C validator