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

Theorem cnm 7754
Description: A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.)
Assertion
Ref Expression
cnm (𝐴 ∈ ℂ → ∃𝑥 𝑥𝐴)
Distinct variable group:   𝑥,𝐴

Proof of Theorem cnm
Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxpi 4604 . . 3 (𝐴 ∈ (R × R) → ∃𝑢𝑣(𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R)))
2 df-c 7740 . . 3 ℂ = (R × R)
31, 2eleq2s 2252 . 2 (𝐴 ∈ ℂ → ∃𝑢𝑣(𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R)))
4 vex 2715 . . . . . 6 𝑢 ∈ V
5 vex 2715 . . . . . 6 𝑣 ∈ V
6 opm 4196 . . . . . 6 (∃𝑥 𝑥 ∈ ⟨𝑢, 𝑣⟩ ↔ (𝑢 ∈ V ∧ 𝑣 ∈ V))
74, 5, 6mpbir2an 927 . . . . 5 𝑥 𝑥 ∈ ⟨𝑢, 𝑣
8 simprl 521 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R))) → 𝐴 = ⟨𝑢, 𝑣⟩)
98eleq2d 2227 . . . . . 6 ((𝐴 ∈ ℂ ∧ (𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R))) → (𝑥𝐴𝑥 ∈ ⟨𝑢, 𝑣⟩))
109exbidv 1805 . . . . 5 ((𝐴 ∈ ℂ ∧ (𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R))) → (∃𝑥 𝑥𝐴 ↔ ∃𝑥 𝑥 ∈ ⟨𝑢, 𝑣⟩))
117, 10mpbiri 167 . . . 4 ((𝐴 ∈ ℂ ∧ (𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R))) → ∃𝑥 𝑥𝐴)
1211ex 114 . . 3 (𝐴 ∈ ℂ → ((𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R)) → ∃𝑥 𝑥𝐴))
1312exlimdvv 1877 . 2 (𝐴 ∈ ℂ → (∃𝑢𝑣(𝐴 = ⟨𝑢, 𝑣⟩ ∧ (𝑢R𝑣R)) → ∃𝑥 𝑥𝐴))
143, 13mpd 13 1 (𝐴 ∈ ℂ → ∃𝑥 𝑥𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1335  wex 1472  wcel 2128  Vcvv 2712  cop 3564   × cxp 4586  Rcnr 7219  cc 7732
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-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4084  ax-pow 4137
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3546  df-sn 3567  df-pr 3568  df-op 3570  df-opab 4028  df-xp 4594  df-c 7740
This theorem is referenced by:  axaddf  7790  axmulf  7791
  Copyright terms: Public domain W3C validator