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

Theorem nqprlu 6395
 Description: The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
Assertion
Ref Expression
nqprlu (A Q → ⟨{xx <Q A}, {xA <Q x}⟩ P)
Distinct variable group:   x,A

Proof of Theorem nqprlu
Dummy variables 𝑟 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nqprm 6391 . . 3 (A Q → (𝑞 Q 𝑞 {xx <Q A} 𝑟 Q 𝑟 {xA <Q x}))
2 ltrelnq 6218 . . . . . . 7 <Q ⊆ (Q × Q)
32brel 4315 . . . . . 6 (x <Q A → (x Q A Q))
43simpld 105 . . . . 5 (x <Q Ax Q)
54abssi 2988 . . . 4 {xx <Q A} ⊆ Q
62brel 4315 . . . . . 6 (A <Q x → (A Q x Q))
76simprd 107 . . . . 5 (A <Q xx Q)
87abssi 2988 . . . 4 {xA <Q x} ⊆ Q
95, 8pm3.2i 257 . . 3 ({xx <Q A} ⊆ Q {xA <Q x} ⊆ Q)
101, 9jctil 295 . 2 (A Q → (({xx <Q A} ⊆ Q {xA <Q x} ⊆ Q) (𝑞 Q 𝑞 {xx <Q A} 𝑟 Q 𝑟 {xA <Q x})))
11 nqprrnd 6392 . . 3 (A Q → (𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A})) 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))))
12 nqprdisj 6393 . . 3 (A Q𝑞 Q ¬ (𝑞 {xx <Q A} 𝑞 {xA <Q x}))
13 nqprloc 6394 . . 3 (A Q𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))
1411, 12, 133jca 1067 . 2 (A Q → ((𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A})) 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))) 𝑞 Q ¬ (𝑞 {xx <Q A} 𝑞 {xA <Q x}) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x}))))
15 elinp 6322 . 2 (⟨{xx <Q A}, {xA <Q x}⟩ P ↔ ((({xx <Q A} ⊆ Q {xA <Q x} ⊆ Q) (𝑞 Q 𝑞 {xx <Q A} 𝑟 Q 𝑟 {xA <Q x})) ((𝑞 Q (𝑞 {xx <Q A} ↔ 𝑟 Q (𝑞 <Q 𝑟 𝑟 {xx <Q A})) 𝑟 Q (𝑟 {xA <Q x} ↔ 𝑞 Q (𝑞 <Q 𝑟 𝑞 {xA <Q x}))) 𝑞 Q ¬ (𝑞 {xx <Q A} 𝑞 {xA <Q x}) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 {xx <Q A} 𝑟 {xA <Q x})))))
1610, 14, 15sylanbrc 396 1 (A Q → ⟨{xx <Q A}, {xA <Q x}⟩ P)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 871   ∈ wcel 1370  {cab 2004  ∀wral 2280  ∃wrex 2281   ⊆ wss 2890  ⟨cop 3349   class class class wbr 3734  Qcnq 6134
 Copyright terms: Public domain W3C validator