cnref1o - Intuitionistic Logic Explorer

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

Theorem cnref1o 9613

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 7784), 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 108	. . . . . . . 8 $/\$
2	1	recnd 7952	. . . . . . 7 $/\$
3		ax-icn 7873	. . . . . . . . 9
4	3	a1i 9	. . . . . . . 8 $/\$
5		simpr 109	. . . . . . . . 9 $/\$
6	5	recnd 7952	. . . . . . . 8 $/\$
7	4, 6	mulcld 7944	. . . . . . 7 $/\$
8	2, 7	addcld 7943	. . . . . 6 $/\$
9	8	rgen2a 2525	. . . . 5
10		cnref1o.1	. . . . . 6
11	10	fnmpo 6185	. . . . 5
12	9, 11	ax-mp 5	. . . 4
13		1st2nd2 6158	. . . . . . . . 9
14	13	fveq2d 5503	. . . . . . . 8
15		df-ov 5860	. . . . . . . 8
16	14, 15	eqtr4di 2222	. . . . . . 7
17		xp1st 6148	. . . . . . . 8
18		xp2nd 6149	. . . . . . . 8
19	17	recnd 7952	. . . . . . . . 9
20	3	a1i 9	. . . . . . . . . 10
21	18	recnd 7952	. . . . . . . . . 10
22	20, 21	mulcld 7944	. . . . . . . . 9
23	19, 22	addcld 7943	. . . . . . . 8
24		oveq1 5864	. . . . . . . . 9
25		oveq2 5865	. . . . . . . . . 10
26	25	oveq2d 5873	. . . . . . . . 9
27	24, 26, 10	ovmpog 5991	. . . . . . . 8 $/\$ $/\$
28	17, 18, 23, 27	syl3anc 1234	. . . . . . 7
29	16, 28	eqtrd 2204	. . . . . 6
30	29, 23	eqeltrd 2248	. . . . 5
31	30	rgen 2524	. . . 4
32		ffnfv 5658	. . . 4 $/\$
33	12, 31, 32	mpbir2an 938	. . 3
34	17, 18	jca 304	. . . . . . 7 $/\$
35		xp1st 6148	. . . . . . . 8
36		xp2nd 6149	. . . . . . . 8
37	35, 36	jca 304	. . . . . . 7 $/\$
38		cru 8525	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
39	34, 37, 38	syl2an 287	. . . . . 6 $/\$ $/\$
40		fveq2 5499	. . . . . . . . 9
41		fveq2 5499	. . . . . . . . . 10
42		fveq2 5499	. . . . . . . . . . 11
43	42	oveq2d 5873	. . . . . . . . . 10
44	41, 43	oveq12d 5875	. . . . . . . . 9
45	40, 44	eqeq12d 2186	. . . . . . . 8
46	45, 29	vtoclga 2797	. . . . . . 7
47	29, 46	eqeqan12d 2187	. . . . . 6 $/\$
48		1st2nd2 6158	. . . . . . . 8
49	13, 48	eqeqan12d 2187	. . . . . . 7 $/\$
50		vex 2734	. . . . . . . . 9
51		1stexg 6150	. . . . . . . . 9
52	50, 51	ax-mp 5	. . . . . . . 8
53		2ndexg 6151	. . . . . . . . 9
54	50, 53	ax-mp 5	. . . . . . . 8
55	52, 54	opth 4223	. . . . . . 7 $/\$
56	49, 55	bitrdi 195	. . . . . 6 $/\$ $/\$
57	39, 47, 56	3bitr4d 219	. . . . 5 $/\$
58	57	biimpd 143	. . . 4 $/\$
59	58	rgen2a 2525	. . 3
60		dff13 5751	. . 3 $/\$
61	33, 59, 60	mpbir2an 938	. 2
62		cnre 7920	. . . . . 6
63		simpl 108	. . . . . . . . 9 $/\$
64		simpr 109	. . . . . . . . 9 $/\$
65	63	recnd 7952	. . . . . . . . . 10 $/\$
66	3	a1i 9	. . . . . . . . . . 11 $/\$
67	64	recnd 7952	. . . . . . . . . . 11 $/\$
68	66, 67	mulcld 7944	. . . . . . . . . 10 $/\$
69	65, 68	addcld 7943	. . . . . . . . 9 $/\$
70		oveq1 5864	. . . . . . . . . 10
71		oveq2 5865	. . . . . . . . . . 11
72	71	oveq2d 5873	. . . . . . . . . 10
73	70, 72, 10	ovmpog 5991	. . . . . . . . 9 $/\$ $/\$
74	63, 64, 69, 73	syl3anc 1234	. . . . . . . 8 $/\$
75	74	eqeq2d 2183	. . . . . . 7 $/\$
76	75	2rexbiia 2487	. . . . . 6
77	62, 76	sylibr 133	. . . . 5
78		fveq2 5499	. . . . . . . 8
79		df-ov 5860	. . . . . . . 8
80	78, 79	eqtr4di 2222	. . . . . . 7
81	80	eqeq2d 2183	. . . . . 6
82	81	rexxp 4756	. . . . 5
83	77, 82	sylibr 133	. . . 4
84	83	rgen 2524	. . 3
85		dffo3 5647	. . 3 $/\$
86	33, 84, 85	mpbir2an 938	. 2
87		df-f1o 5207	. 2 $/\$
88	61, 86, 87	mpbir2an 938	1

Colors of variables: wff set class

Syntax hints:

wi 4 $/\$ wa 103

wb 104

wceq 1349

wcel 2142

wral 2449

wrex 2450

cvv 2731

cop 3587

cxp 4610

wfn 5195

wf 5196

wf1 5197

wfo 5198

wf1o 5199

cfv 5200 (class class class)co 5857

cmpo 5859

c1st 6121

c2nd 6122

cc 7776

cr 7777

ci 7780

caddc 7781

cmul 7783

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 610 ax-in2 611 ax-io 705 ax-5 1441 ax-7 1442 ax-gen 1443 ax-ie1 1487 ax-ie2 1488 ax-8 1498 ax-10 1499 ax-11 1500 ax-i12 1501 ax-bndl 1503 ax-4 1504 ax-17 1520 ax-i9 1524 ax-ial 1528 ax-i5r 1529 ax-13 2144 ax-14 2145 ax-ext 2153 ax-sep 4108 ax-pow 4161 ax-pr 4195 ax-un 4419 ax-setind 4522 ax-cnex 7869 ax-resscn 7870 ax-1cn 7871 ax-1re 7872 ax-icn 7873 ax-addcl 7874 ax-addrcl 7875 ax-mulcl 7876 ax-mulrcl 7877 ax-addcom 7878 ax-mulcom 7879 ax-addass 7880 ax-mulass 7881 ax-distr 7882 ax-i2m1 7883 ax-0lt1 7884 ax-1rid 7885 ax-0id 7886 ax-rnegex 7887 ax-precex 7888 ax-cnre 7889 ax-pre-ltirr 7890 ax-pre-lttrn 7892 ax-pre-apti 7893 ax-pre-ltadd 7894 ax-pre-mulgt0 7895

This theorem depends on definitions: df-bi 116 df-3an 976 df-tru 1352 df-fal 1355 df-nf 1455 df-sb 1757 df-eu 2023 df-mo 2024 df-clab 2158 df-cleq 2164 df-clel 2167 df-nfc 2302 df-ne 2342 df-nel 2437 df-ral 2454 df-rex 2455 df-reu 2456 df-rab 2458 df-v 2733 df-sbc 2957 df-csb 3051 df-dif 3124 df-un 3126 df-in 3128 df-ss 3135 df-pw 3569 df-sn 3590 df-pr 3591 df-op 3593 df-uni 3798 df-iun 3876 df-br 3991 df-opab 4052 df-mpt 4053 df-id 4279 df-xp 4618 df-rel 4619 df-cnv 4620 df-co 4621 df-dm 4622 df-rn 4623 df-res 4624 df-ima 4625 df-iota 5162 df-fun 5202 df-fn 5203 df-f 5204 df-f1 5205 df-fo 5206 df-f1o 5207 df-fv 5208 df-riota 5813 df-ov 5860 df-oprab 5861 df-mpo 5862 df-1st 6123 df-2nd 6124 df-pnf 7960 df-mnf 7961 df-ltxr 7963 df-sub 8096 df-neg 8097 df-reap 8498

This theorem is referenced by: cnrecnv 10878

W3C validator