Theorem cnref1o 8733

Description: There is a natural one-to-one mapping from (ℝ × ℝ) to ℂ, where we map ⟨𝑥, 𝑦⟩ to (𝑥 + (i · 𝑦)). In our construction of the complex numbers, this is in fact our definition of ℂ (see df-c 6987), 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	⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))

Assertion

Ref	Expression
cnref1o	⊢ 𝐹:(ℝ × ℝ)–1-1-onto→ℂ

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 7147	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
3		ax-icn 7071	. . . . . . . . 9 ⊢ i ∈ ℂ
4	3	a1i 9	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
5		simpr 108	. . . . . . . . 9 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
6	5	recnd 7147	. . . . . . . 8 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
7	4, 6	mulcld 7139	. . . . . . 7 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i · 𝑦) ∈ ℂ)
8	2, 7	addcld 7138	. . . . . 6 ⊢ ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + (i · 𝑦)) ∈ ℂ)
9	8	rgen2a 2417	. . . . 5 ⊢ ∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 + (i · 𝑦)) ∈ ℂ
10		cnref1o.1	. . . . . 6 ⊢ 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))
11	10	fnmpt2 5848	. . . . 5 ⊢ (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 + (i · 𝑦)) ∈ ℂ → 𝐹 Fn (ℝ × ℝ))
12	9, 11	ax-mp 7	. . . 4 ⊢ 𝐹 Fn (ℝ × ℝ)
13		1st2nd2 5821	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
14	13	fveq2d 5202	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = (𝐹‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩))
15		df-ov 5535	. . . . . . . 8 ⊢ ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = (𝐹‘⟨(1st ‘𝑧), (2nd ‘𝑧)⟩)
16	14, 15	syl6eqr 2131	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = ((1st ‘𝑧)𝐹(2nd ‘𝑧)))
17		xp1st 5812	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1st ‘𝑧) ∈ ℝ)
18		xp2nd 5813	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2nd ‘𝑧) ∈ ℝ)
19	17	recnd 7147	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℝ × ℝ) → (1st ‘𝑧) ∈ ℂ)
20	3	a1i 9	. . . . . . . . . 10 ⊢ (𝑧 ∈ (ℝ × ℝ) → i ∈ ℂ)
21	18	recnd 7147	. . . . . . . . . 10 ⊢ (𝑧 ∈ (ℝ × ℝ) → (2nd ‘𝑧) ∈ ℂ)
22	20, 21	mulcld 7139	. . . . . . . . 9 ⊢ (𝑧 ∈ (ℝ × ℝ) → (i · (2nd ‘𝑧)) ∈ ℂ)
23	19, 22	addcld 7138	. . . . . . . 8 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1st ‘𝑧) + (i · (2nd ‘𝑧))) ∈ ℂ)
24		oveq1 5539	. . . . . . . . 9 ⊢ (𝑥 = (1st ‘𝑧) → (𝑥 + (i · 𝑦)) = ((1st ‘𝑧) + (i · 𝑦)))
25		oveq2 5540	. . . . . . . . . 10 ⊢ (𝑦 = (2nd ‘𝑧) → (i · 𝑦) = (i · (2nd ‘𝑧)))
26	25	oveq2d 5548	. . . . . . . . 9 ⊢ (𝑦 = (2nd ‘𝑧) → ((1st ‘𝑧) + (i · 𝑦)) = ((1st ‘𝑧) + (i · (2nd ‘𝑧))))
27	24, 26, 10	ovmpt2g 5655	. . . . . . . 8 ⊢ (((1st ‘𝑧) ∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ ∧ ((1st ‘𝑧) + (i · (2nd ‘𝑧))) ∈ ℂ) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = ((1st ‘𝑧) + (i · (2nd ‘𝑧))))
28	17, 18, 23, 27	syl3anc 1169	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1st ‘𝑧)𝐹(2nd ‘𝑧)) = ((1st ‘𝑧) + (i · (2nd ‘𝑧))))
29	16, 28	eqtrd 2113	. . . . . 6 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) = ((1st ‘𝑧) + (i · (2nd ‘𝑧))))
30	29, 23	eqeltrd 2155	. . . . 5 ⊢ (𝑧 ∈ (ℝ × ℝ) → (𝐹‘𝑧) ∈ ℂ)
31	30	rgen 2416	. . . 4 ⊢ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ ℂ
32		ffnfv 5344	. . . 4 ⊢ (𝐹:(ℝ × ℝ)⟶ℂ ↔ (𝐹 Fn (ℝ × ℝ) ∧ ∀𝑧 ∈ (ℝ × ℝ)(𝐹‘𝑧) ∈ ℂ))
33	12, 31, 32	mpbir2an 883	. . 3 ⊢ 𝐹:(ℝ × ℝ)⟶ℂ
34	17, 18	jca 300	. . . . . . 7 ⊢ (𝑧 ∈ (ℝ × ℝ) → ((1st ‘𝑧) ∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ))
35		xp1st 5812	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (1st ‘𝑤) ∈ ℝ)
36		xp2nd 5813	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → (2nd ‘𝑤) ∈ ℝ)
37	35, 36	jca 300	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → ((1st ‘𝑤) ∈ ℝ ∧ (2nd ‘𝑤) ∈ ℝ))
38		cru 7702	. . . . . . 7 ⊢ ((((1st ‘𝑧) ∈ ℝ ∧ (2nd ‘𝑧) ∈ ℝ) ∧ ((1st ‘𝑤) ∈ ℝ ∧ (2nd ‘𝑤) ∈ ℝ)) → (((1st ‘𝑧) + (i · (2nd ‘𝑧))) = ((1st ‘𝑤) + (i · (2nd ‘𝑤))) ↔ ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤))))
39	34, 37, 38	syl2an 283	. . . . . 6 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (((1st ‘𝑧) + (i · (2nd ‘𝑧))) = ((1st ‘𝑤) + (i · (2nd ‘𝑤))) ↔ ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤))))
40		fveq2 5198	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → (𝐹‘𝑧) = (𝐹‘𝑤))
41		fveq2 5198	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (1st ‘𝑧) = (1st ‘𝑤))
42		fveq2 5198	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑤 → (2nd ‘𝑧) = (2nd ‘𝑤))
43	42	oveq2d 5548	. . . . . . . . . 10 ⊢ (𝑧 = 𝑤 → (i · (2nd ‘𝑧)) = (i · (2nd ‘𝑤)))
44	41, 43	oveq12d 5550	. . . . . . . . 9 ⊢ (𝑧 = 𝑤 → ((1st ‘𝑧) + (i · (2nd ‘𝑧))) = ((1st ‘𝑤) + (i · (2nd ‘𝑤))))
45	40, 44	eqeq12d 2095	. . . . . . . 8 ⊢ (𝑧 = 𝑤 → ((𝐹‘𝑧) = ((1st ‘𝑧) + (i · (2nd ‘𝑧))) ↔ (𝐹‘𝑤) = ((1st ‘𝑤) + (i · (2nd ‘𝑤)))))
46	45, 29	vtoclga 2664	. . . . . . 7 ⊢ (𝑤 ∈ (ℝ × ℝ) → (𝐹‘𝑤) = ((1st ‘𝑤) + (i · (2nd ‘𝑤))))
47	29, 46	eqeqan12d 2096	. . . . . 6 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ ((1st ‘𝑧) + (i · (2nd ‘𝑧))) = ((1st ‘𝑤) + (i · (2nd ‘𝑤)))))
48		1st2nd2 5821	. . . . . . . 8 ⊢ (𝑤 ∈ (ℝ × ℝ) → 𝑤 = ⟨(1st ‘𝑤), (2nd ‘𝑤)⟩)
49	13, 48	eqeqan12d 2096	. . . . . . 7 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ = ⟨(1st ‘𝑤), (2nd ‘𝑤)⟩))
50		vex 2604	. . . . . . . . 9 ⊢ 𝑧 ∈ V
51		1stexg 5814	. . . . . . . . 9 ⊢ (𝑧 ∈ V → (1st ‘𝑧) ∈ V)
52	50, 51	ax-mp 7	. . . . . . . 8 ⊢ (1st ‘𝑧) ∈ V
53		2ndexg 5815	. . . . . . . . 9 ⊢ (𝑧 ∈ V → (2nd ‘𝑧) ∈ V)
54	50, 53	ax-mp 7	. . . . . . . 8 ⊢ (2nd ‘𝑧) ∈ V
55	52, 54	opth 3992	. . . . . . 7 ⊢ (⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ = ⟨(1st ‘𝑤), (2nd ‘𝑤)⟩ ↔ ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤)))
56	49, 55	syl6bb 194	. . . . . 6 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ((1st ‘𝑧) = (1st ‘𝑤) ∧ (2nd ‘𝑧) = (2nd ‘𝑤))))
57	39, 47, 56	3bitr4d 218	. . . . 5 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) ↔ 𝑧 = 𝑤))
58	57	biimpd 142	. . . 4 ⊢ ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤))
59	58	rgen2a 2417	. . 3 ⊢ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)
60		dff13 5428	. . 3 ⊢ (𝐹:(ℝ × ℝ)–1-1→ℂ ↔ (𝐹:(ℝ × ℝ)⟶ℂ ∧ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹‘𝑧) = (𝐹‘𝑤) → 𝑧 = 𝑤)))
61	33, 59, 60	mpbir2an 883	. 2 ⊢ 𝐹:(ℝ × ℝ)–1-1→ℂ
62		cnre 7115	. . . . . 6 ⊢ (𝑤 ∈ ℂ → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢 + (i · 𝑣)))
63		simpl 107	. . . . . . . . 9 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑢 ∈ ℝ)
64		simpr 108	. . . . . . . . 9 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑣 ∈ ℝ)
65	63	recnd 7147	. . . . . . . . . 10 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑢 ∈ ℂ)
66	3	a1i 9	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → i ∈ ℂ)
67	64	recnd 7147	. . . . . . . . . . 11 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑣 ∈ ℂ)
68	66, 67	mulcld 7139	. . . . . . . . . 10 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (i · 𝑣) ∈ ℂ)
69	65, 68	addcld 7138	. . . . . . . . 9 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢 + (i · 𝑣)) ∈ ℂ)
70		oveq1 5539	. . . . . . . . . 10 ⊢ (𝑥 = 𝑢 → (𝑥 + (i · 𝑦)) = (𝑢 + (i · 𝑦)))
71		oveq2 5540	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑣 → (i · 𝑦) = (i · 𝑣))
72	71	oveq2d 5548	. . . . . . . . . 10 ⊢ (𝑦 = 𝑣 → (𝑢 + (i · 𝑦)) = (𝑢 + (i · 𝑣)))
73	70, 72, 10	ovmpt2g 5655	. . . . . . . . 9 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ (𝑢 + (i · 𝑣)) ∈ ℂ) → (𝑢𝐹𝑣) = (𝑢 + (i · 𝑣)))
74	63, 64, 69, 73	syl3anc 1169	. . . . . . . 8 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢𝐹𝑣) = (𝑢 + (i · 𝑣)))
75	74	eqeq2d 2092	. . . . . . 7 ⊢ ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑤 = (𝑢𝐹𝑣) ↔ 𝑤 = (𝑢 + (i · 𝑣))))
76	75	2rexbiia 2382	. . . . . 6 ⊢ (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢 + (i · 𝑣)))
77	62, 76	sylibr 132	. . . . 5 ⊢ (𝑤 ∈ ℂ → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
78		fveq2 5198	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝐹‘⟨𝑢, 𝑣⟩))
79		df-ov 5535	. . . . . . . 8 ⊢ (𝑢𝐹𝑣) = (𝐹‘⟨𝑢, 𝑣⟩)
80	78, 79	syl6eqr 2131	. . . . . . 7 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹‘𝑧) = (𝑢𝐹𝑣))
81	80	eqeq2d 2092	. . . . . 6 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑤 = (𝐹‘𝑧) ↔ 𝑤 = (𝑢𝐹𝑣)))
82	81	rexxp 4498	. . . . 5 ⊢ (∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
83	77, 82	sylibr 132	. . . 4 ⊢ (𝑤 ∈ ℂ → ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧))
84	83	rgen 2416	. . 3 ⊢ ∀𝑤 ∈ ℂ ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)
85		dffo3 5335	. . 3 ⊢ (𝐹:(ℝ × ℝ)–onto→ℂ ↔ (𝐹:(ℝ × ℝ)⟶ℂ ∧ ∀𝑤 ∈ ℂ ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹‘𝑧)))
86	33, 84, 85	mpbir2an 883	. 2 ⊢ 𝐹:(ℝ × ℝ)–onto→ℂ
87		df-f1o 4929	. 2 ⊢ (𝐹:(ℝ × ℝ)–1-1-onto→ℂ ↔ (𝐹:(ℝ × ℝ)–1-1→ℂ ∧ 𝐹:(ℝ × ℝ)–onto→ℂ))
88	61, 86, 87	mpbir2an 883	1 ⊢ 𝐹:(ℝ × ℝ)–1-1-onto→ℂ

Syntax hints:   → wi 4   ∧ wa 102   ↔ wb 103   = wceq 1284   ∈ wcel 1433  ∀wral 2348  ∃wrex 2349  Vcvv 2601  ⟨cop 3401   × cxp 4361   Fn wfn 4917  ⟶wf 4918  –1-1→wf1 4919  –onto→wfo 4920  –1-1-onto→wf1o 4921  ‘cfv 4922  (class class class)co 5532   ↦ cmpt2 5534  1^st c1st 5785  2^nd c2nd 5786  ℂcc 6979  ℝcr 6980  ici 6983   + caddc 6984   · cmul 6986

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 576  ax-in2 577  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-13 1444  ax-14 1445  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063  ax-sep 3896  ax-pow 3948  ax-pr 3964  ax-un 4188  ax-setind 4280  ax-cnex 7067  ax-resscn 7068  ax-1cn 7069  ax-1re 7070  ax-icn 7071  ax-addcl 7072  ax-addrcl 7073  ax-mulcl 7074  ax-mulrcl 7075  ax-addcom 7076  ax-mulcom 7077  ax-addass 7078  ax-mulass 7079  ax-distr 7080  ax-i2m1 7081  ax-0lt1 7082  ax-1rid 7083  ax-0id 7084  ax-rnegex 7085  ax-precex 7086  ax-cnre 7087  ax-pre-ltirr 7088  ax-pre-lttrn 7090  ax-pre-apti 7091  ax-pre-ltadd 7092  ax-pre-mulgt0 7093

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-fal 1290  df-nf 1390  df-sb 1686  df-eu 1944  df-mo 1945  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ne 2246  df-nel 2340  df-ral 2353  df-rex 2354  df-reu 2355  df-rab 2357  df-v 2603  df-sbc 2816  df-csb 2909  df-dif 2975  df-un 2977  df-in 2979  df-ss 2986  df-pw 3384  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-iun 3680  df-br 3786  df-opab 3840  df-mpt 3841  df-id 4048  df-xp 4369  df-rel 4370  df-cnv 4371  df-co 4372  df-dm 4373  df-rn 4374  df-res 4375  df-ima 4376  df-iota 4887  df-fun 4924  df-fn 4925  df-f 4926  df-f1 4927  df-fo 4928  df-f1o 4929  df-fv 4930  df-riota 5488  df-ov 5535  df-oprab 5536  df-mpt2 5537  df-1st 5787  df-2nd 5788  df-pnf 7155  df-mnf 7156  df-ltxr 7158  df-sub 7281  df-neg 7282  df-reap 7675

This theorem is referenced by:  cnrecnv  9797