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

Theorem nnnq 6709
Description: The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.)
Assertion
Ref Expression
nnnq (𝐴N → [⟨𝐴, 1𝑜⟩] ~QQ)

Proof of Theorem nnnq
StepHypRef Expression
1 1pi 6602 . . . 4 1𝑜N
2 opelxpi 4422 . . . 4 ((𝐴N ∧ 1𝑜N) → ⟨𝐴, 1𝑜⟩ ∈ (N × N))
31, 2mpan2 416 . . 3 (𝐴N → ⟨𝐴, 1𝑜⟩ ∈ (N × N))
4 enqex 6647 . . . 4 ~Q ∈ V
54ecelqsi 6247 . . 3 (⟨𝐴, 1𝑜⟩ ∈ (N × N) → [⟨𝐴, 1𝑜⟩] ~Q ∈ ((N × N) / ~Q ))
63, 5syl 14 . 2 (𝐴N → [⟨𝐴, 1𝑜⟩] ~Q ∈ ((N × N) / ~Q ))
7 df-nqqs 6635 . 2 Q = ((N × N) / ~Q )
86, 7syl6eleqr 2176 1 (𝐴N → [⟨𝐴, 1𝑜⟩] ~QQ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  cop 3419   × cxp 4389  1𝑜c1o 6078  [cec 6191   / cqs 6192  Ncnpi 6559   ~Q ceq 6566  Qcnq 6567
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 3916  ax-nul 3924  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-iinf 4357
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  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-ral 2358  df-rex 2359  df-v 2611  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-int 3657  df-br 3806  df-opab 3860  df-suc 4154  df-iom 4360  df-xp 4397  df-cnv 4399  df-dm 4401  df-rn 4402  df-res 4403  df-ima 4404  df-1o 6085  df-ec 6195  df-qs 6199  df-ni 6591  df-enq 6634  df-nqqs 6635
This theorem is referenced by:  recnnpr  6835  nnprlu  6840  archrecnq  6950  archrecpr  6951  caucvgprlemnkj  6953  caucvgprlemnbj  6954  caucvgprlemm  6955  caucvgprlemopl  6956  caucvgprlemlol  6957  caucvgprlemloc  6962  caucvgprlemladdfu  6964  caucvgprlemladdrl  6965  caucvgprprlemloccalc  6971  caucvgprprlemnkltj  6976  caucvgprprlemnkeqj  6977  caucvgprprlemnjltk  6978  caucvgprprlemml  6981  caucvgprprlemopl  6984  caucvgprprlemlol  6985  caucvgprprlemloc  6990  caucvgprprlemexb  6994  caucvgprprlem1  6996  caucvgprprlem2  6997  pitonnlem2  7112  ltrennb  7119  recidpipr  7121
  Copyright terms: Public domain W3C validator