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

Theorem cnref1o 9027
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 7258), 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.
StepHypRef Expression
1 simpl 107 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℝ)
21recnd 7418 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑥 ∈ ℂ)
3 ax-icn 7342 . . . . . . . . 9 i ∈ ℂ
43a1i 9 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → i ∈ ℂ)
5 simpr 108 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
65recnd 7418 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℂ)
74, 6mulcld 7410 . . . . . . 7 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (i · 𝑦) ∈ ℂ)
82, 7addcld 7409 . . . . . 6 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 + (i · 𝑦)) ∈ ℂ)
98rgen2a 2423 . . . . 5 𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 + (i · 𝑦)) ∈ ℂ
10 cnref1o.1 . . . . . 6 𝐹 = (𝑥 ∈ ℝ, 𝑦 ∈ ℝ ↦ (𝑥 + (i · 𝑦)))
1110fnmpt2 5906 . . . . 5 (∀𝑥 ∈ ℝ ∀𝑦 ∈ ℝ (𝑥 + (i · 𝑦)) ∈ ℂ → 𝐹 Fn (ℝ × ℝ))
129, 11ax-mp 7 . . . 4 𝐹 Fn (ℝ × ℝ)
13 1st2nd2 5879 . . . . . . . . 9 (𝑧 ∈ (ℝ × ℝ) → 𝑧 = ⟨(1st𝑧), (2nd𝑧)⟩)
1413fveq2d 5256 . . . . . . . 8 (𝑧 ∈ (ℝ × ℝ) → (𝐹𝑧) = (𝐹‘⟨(1st𝑧), (2nd𝑧)⟩))
15 df-ov 5593 . . . . . . . 8 ((1st𝑧)𝐹(2nd𝑧)) = (𝐹‘⟨(1st𝑧), (2nd𝑧)⟩)
1614, 15syl6eqr 2133 . . . . . . 7 (𝑧 ∈ (ℝ × ℝ) → (𝐹𝑧) = ((1st𝑧)𝐹(2nd𝑧)))
17 xp1st 5870 . . . . . . . 8 (𝑧 ∈ (ℝ × ℝ) → (1st𝑧) ∈ ℝ)
18 xp2nd 5871 . . . . . . . 8 (𝑧 ∈ (ℝ × ℝ) → (2nd𝑧) ∈ ℝ)
1917recnd 7418 . . . . . . . . 9 (𝑧 ∈ (ℝ × ℝ) → (1st𝑧) ∈ ℂ)
203a1i 9 . . . . . . . . . 10 (𝑧 ∈ (ℝ × ℝ) → i ∈ ℂ)
2118recnd 7418 . . . . . . . . . 10 (𝑧 ∈ (ℝ × ℝ) → (2nd𝑧) ∈ ℂ)
2220, 21mulcld 7410 . . . . . . . . 9 (𝑧 ∈ (ℝ × ℝ) → (i · (2nd𝑧)) ∈ ℂ)
2319, 22addcld 7409 . . . . . . . 8 (𝑧 ∈ (ℝ × ℝ) → ((1st𝑧) + (i · (2nd𝑧))) ∈ ℂ)
24 oveq1 5597 . . . . . . . . 9 (𝑥 = (1st𝑧) → (𝑥 + (i · 𝑦)) = ((1st𝑧) + (i · 𝑦)))
25 oveq2 5598 . . . . . . . . . 10 (𝑦 = (2nd𝑧) → (i · 𝑦) = (i · (2nd𝑧)))
2625oveq2d 5606 . . . . . . . . 9 (𝑦 = (2nd𝑧) → ((1st𝑧) + (i · 𝑦)) = ((1st𝑧) + (i · (2nd𝑧))))
2724, 26, 10ovmpt2g 5713 . . . . . . . 8 (((1st𝑧) ∈ ℝ ∧ (2nd𝑧) ∈ ℝ ∧ ((1st𝑧) + (i · (2nd𝑧))) ∈ ℂ) → ((1st𝑧)𝐹(2nd𝑧)) = ((1st𝑧) + (i · (2nd𝑧))))
2817, 18, 23, 27syl3anc 1170 . . . . . . 7 (𝑧 ∈ (ℝ × ℝ) → ((1st𝑧)𝐹(2nd𝑧)) = ((1st𝑧) + (i · (2nd𝑧))))
2916, 28eqtrd 2115 . . . . . 6 (𝑧 ∈ (ℝ × ℝ) → (𝐹𝑧) = ((1st𝑧) + (i · (2nd𝑧))))
3029, 23eqeltrd 2159 . . . . 5 (𝑧 ∈ (ℝ × ℝ) → (𝐹𝑧) ∈ ℂ)
3130rgen 2422 . . . 4 𝑧 ∈ (ℝ × ℝ)(𝐹𝑧) ∈ ℂ
32 ffnfv 5397 . . . 4 (𝐹:(ℝ × ℝ)⟶ℂ ↔ (𝐹 Fn (ℝ × ℝ) ∧ ∀𝑧 ∈ (ℝ × ℝ)(𝐹𝑧) ∈ ℂ))
3312, 31, 32mpbir2an 884 . . 3 𝐹:(ℝ × ℝ)⟶ℂ
3417, 18jca 300 . . . . . . 7 (𝑧 ∈ (ℝ × ℝ) → ((1st𝑧) ∈ ℝ ∧ (2nd𝑧) ∈ ℝ))
35 xp1st 5870 . . . . . . . 8 (𝑤 ∈ (ℝ × ℝ) → (1st𝑤) ∈ ℝ)
36 xp2nd 5871 . . . . . . . 8 (𝑤 ∈ (ℝ × ℝ) → (2nd𝑤) ∈ ℝ)
3735, 36jca 300 . . . . . . 7 (𝑤 ∈ (ℝ × ℝ) → ((1st𝑤) ∈ ℝ ∧ (2nd𝑤) ∈ ℝ))
38 cru 7978 . . . . . . 7 ((((1st𝑧) ∈ ℝ ∧ (2nd𝑧) ∈ ℝ) ∧ ((1st𝑤) ∈ ℝ ∧ (2nd𝑤) ∈ ℝ)) → (((1st𝑧) + (i · (2nd𝑧))) = ((1st𝑤) + (i · (2nd𝑤))) ↔ ((1st𝑧) = (1st𝑤) ∧ (2nd𝑧) = (2nd𝑤))))
3934, 37, 38syl2an 283 . . . . . 6 ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (((1st𝑧) + (i · (2nd𝑧))) = ((1st𝑤) + (i · (2nd𝑤))) ↔ ((1st𝑧) = (1st𝑤) ∧ (2nd𝑧) = (2nd𝑤))))
40 fveq2 5252 . . . . . . . . 9 (𝑧 = 𝑤 → (𝐹𝑧) = (𝐹𝑤))
41 fveq2 5252 . . . . . . . . . 10 (𝑧 = 𝑤 → (1st𝑧) = (1st𝑤))
42 fveq2 5252 . . . . . . . . . . 11 (𝑧 = 𝑤 → (2nd𝑧) = (2nd𝑤))
4342oveq2d 5606 . . . . . . . . . 10 (𝑧 = 𝑤 → (i · (2nd𝑧)) = (i · (2nd𝑤)))
4441, 43oveq12d 5608 . . . . . . . . 9 (𝑧 = 𝑤 → ((1st𝑧) + (i · (2nd𝑧))) = ((1st𝑤) + (i · (2nd𝑤))))
4540, 44eqeq12d 2097 . . . . . . . 8 (𝑧 = 𝑤 → ((𝐹𝑧) = ((1st𝑧) + (i · (2nd𝑧))) ↔ (𝐹𝑤) = ((1st𝑤) + (i · (2nd𝑤)))))
4645, 29vtoclga 2675 . . . . . . 7 (𝑤 ∈ (ℝ × ℝ) → (𝐹𝑤) = ((1st𝑤) + (i · (2nd𝑤))))
4729, 46eqeqan12d 2098 . . . . . 6 ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹𝑧) = (𝐹𝑤) ↔ ((1st𝑧) + (i · (2nd𝑧))) = ((1st𝑤) + (i · (2nd𝑤)))))
48 1st2nd2 5879 . . . . . . . 8 (𝑤 ∈ (ℝ × ℝ) → 𝑤 = ⟨(1st𝑤), (2nd𝑤)⟩)
4913, 48eqeqan12d 2098 . . . . . . 7 ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ⟨(1st𝑧), (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑤)⟩))
50 vex 2615 . . . . . . . . 9 𝑧 ∈ V
51 1stexg 5872 . . . . . . . . 9 (𝑧 ∈ V → (1st𝑧) ∈ V)
5250, 51ax-mp 7 . . . . . . . 8 (1st𝑧) ∈ V
53 2ndexg 5873 . . . . . . . . 9 (𝑧 ∈ V → (2nd𝑧) ∈ V)
5450, 53ax-mp 7 . . . . . . . 8 (2nd𝑧) ∈ V
5552, 54opth 4027 . . . . . . 7 (⟨(1st𝑧), (2nd𝑧)⟩ = ⟨(1st𝑤), (2nd𝑤)⟩ ↔ ((1st𝑧) = (1st𝑤) ∧ (2nd𝑧) = (2nd𝑤)))
5649, 55syl6bb 194 . . . . . 6 ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → (𝑧 = 𝑤 ↔ ((1st𝑧) = (1st𝑤) ∧ (2nd𝑧) = (2nd𝑤))))
5739, 47, 563bitr4d 218 . . . . 5 ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹𝑧) = (𝐹𝑤) ↔ 𝑧 = 𝑤))
5857biimpd 142 . . . 4 ((𝑧 ∈ (ℝ × ℝ) ∧ 𝑤 ∈ (ℝ × ℝ)) → ((𝐹𝑧) = (𝐹𝑤) → 𝑧 = 𝑤))
5958rgen2a 2423 . . 3 𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹𝑧) = (𝐹𝑤) → 𝑧 = 𝑤)
60 dff13 5486 . . 3 (𝐹:(ℝ × ℝ)–1-1→ℂ ↔ (𝐹:(ℝ × ℝ)⟶ℂ ∧ ∀𝑧 ∈ (ℝ × ℝ)∀𝑤 ∈ (ℝ × ℝ)((𝐹𝑧) = (𝐹𝑤) → 𝑧 = 𝑤)))
6133, 59, 60mpbir2an 884 . 2 𝐹:(ℝ × ℝ)–1-1→ℂ
62 cnre 7386 . . . . . 6 (𝑤 ∈ ℂ → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢 + (i · 𝑣)))
63 simpl 107 . . . . . . . . 9 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑢 ∈ ℝ)
64 simpr 108 . . . . . . . . 9 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑣 ∈ ℝ)
6563recnd 7418 . . . . . . . . . 10 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑢 ∈ ℂ)
663a1i 9 . . . . . . . . . . 11 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → i ∈ ℂ)
6764recnd 7418 . . . . . . . . . . 11 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → 𝑣 ∈ ℂ)
6866, 67mulcld 7410 . . . . . . . . . 10 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (i · 𝑣) ∈ ℂ)
6965, 68addcld 7409 . . . . . . . . 9 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢 + (i · 𝑣)) ∈ ℂ)
70 oveq1 5597 . . . . . . . . . 10 (𝑥 = 𝑢 → (𝑥 + (i · 𝑦)) = (𝑢 + (i · 𝑦)))
71 oveq2 5598 . . . . . . . . . . 11 (𝑦 = 𝑣 → (i · 𝑦) = (i · 𝑣))
7271oveq2d 5606 . . . . . . . . . 10 (𝑦 = 𝑣 → (𝑢 + (i · 𝑦)) = (𝑢 + (i · 𝑣)))
7370, 72, 10ovmpt2g 5713 . . . . . . . . 9 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ (𝑢 + (i · 𝑣)) ∈ ℂ) → (𝑢𝐹𝑣) = (𝑢 + (i · 𝑣)))
7463, 64, 69, 73syl3anc 1170 . . . . . . . 8 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑢𝐹𝑣) = (𝑢 + (i · 𝑣)))
7574eqeq2d 2094 . . . . . . 7 ((𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ) → (𝑤 = (𝑢𝐹𝑣) ↔ 𝑤 = (𝑢 + (i · 𝑣))))
76752rexbiia 2388 . . . . . 6 (∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢 + (i · 𝑣)))
7762, 76sylibr 132 . . . . 5 (𝑤 ∈ ℂ → ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
78 fveq2 5252 . . . . . . . 8 (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹𝑧) = (𝐹‘⟨𝑢, 𝑣⟩))
79 df-ov 5593 . . . . . . . 8 (𝑢𝐹𝑣) = (𝐹‘⟨𝑢, 𝑣⟩)
8078, 79syl6eqr 2133 . . . . . . 7 (𝑧 = ⟨𝑢, 𝑣⟩ → (𝐹𝑧) = (𝑢𝐹𝑣))
8180eqeq2d 2094 . . . . . 6 (𝑧 = ⟨𝑢, 𝑣⟩ → (𝑤 = (𝐹𝑧) ↔ 𝑤 = (𝑢𝐹𝑣)))
8281rexxp 4537 . . . . 5 (∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹𝑧) ↔ ∃𝑢 ∈ ℝ ∃𝑣 ∈ ℝ 𝑤 = (𝑢𝐹𝑣))
8377, 82sylibr 132 . . . 4 (𝑤 ∈ ℂ → ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹𝑧))
8483rgen 2422 . . 3 𝑤 ∈ ℂ ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹𝑧)
85 dffo3 5390 . . 3 (𝐹:(ℝ × ℝ)–onto→ℂ ↔ (𝐹:(ℝ × ℝ)⟶ℂ ∧ ∀𝑤 ∈ ℂ ∃𝑧 ∈ (ℝ × ℝ)𝑤 = (𝐹𝑧)))
8633, 84, 85mpbir2an 884 . 2 𝐹:(ℝ × ℝ)–onto→ℂ
87 df-f1o 4975 . 2 (𝐹:(ℝ × ℝ)–1-1-onto→ℂ ↔ (𝐹:(ℝ × ℝ)–1-1→ℂ ∧ 𝐹:(ℝ × ℝ)–onto→ℂ))
8861, 86, 87mpbir2an 884 1 𝐹:(ℝ × ℝ)–1-1-onto→ℂ
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103   = wceq 1285  wcel 1434  wral 2353  wrex 2354  Vcvv 2612  cop 3425   × cxp 4398   Fn wfn 4963  wf 4964  1-1wf1 4965  ontowfo 4966  1-1-ontowf1o 4967  cfv 4968  (class class class)co 5590  cmpt2 5592  1st c1st 5843  2nd c2nd 5844  cc 7250  cr 7251  ici 7254   + caddc 7255   · cmul 7257
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 2065  ax-sep 3922  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-setind 4315  ax-cnex 7338  ax-resscn 7339  ax-1cn 7340  ax-1re 7341  ax-icn 7342  ax-addcl 7343  ax-addrcl 7344  ax-mulcl 7345  ax-mulrcl 7346  ax-addcom 7347  ax-mulcom 7348  ax-addass 7349  ax-mulass 7350  ax-distr 7351  ax-i2m1 7352  ax-0lt1 7353  ax-1rid 7354  ax-0id 7355  ax-rnegex 7356  ax-precex 7357  ax-cnre 7358  ax-pre-ltirr 7359  ax-pre-lttrn 7361  ax-pre-apti 7362  ax-pre-ltadd 7363  ax-pre-mulgt0 7364
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-nel 2345  df-ral 2358  df-rex 2359  df-reu 2360  df-rab 2362  df-v 2614  df-sbc 2827  df-csb 2920  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-uni 3628  df-iun 3706  df-br 3812  df-opab 3866  df-mpt 3867  df-id 4083  df-xp 4406  df-rel 4407  df-cnv 4408  df-co 4409  df-dm 4410  df-rn 4411  df-res 4412  df-ima 4413  df-iota 4933  df-fun 4970  df-fn 4971  df-f 4972  df-f1 4973  df-fo 4974  df-f1o 4975  df-fv 4976  df-riota 5546  df-ov 5593  df-oprab 5594  df-mpt2 5595  df-1st 5845  df-2nd 5846  df-pnf 7426  df-mnf 7427  df-ltxr 7429  df-sub 7557  df-neg 7558  df-reap 7951
This theorem is referenced by:  cnrecnv  10170
  Copyright terms: Public domain W3C validator