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

Theorem ltbtwnnq 6720
 Description: There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.)
Assertion
Ref Expression
ltbtwnnq (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem ltbtwnnq
StepHypRef Expression
1 df-rex 2359 . 2 (∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵) ↔ ∃𝑥(𝑥Q ∧ (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
2 ltbtwnnqq 6719 . 2 (𝐴 <Q 𝐵 ↔ ∃𝑥Q (𝐴 <Q 𝑥𝑥 <Q 𝐵))
3 ltrelnq 6669 . . . . . . 7 <Q ⊆ (Q × Q)
43brel 4438 . . . . . 6 (𝐴 <Q 𝑥 → (𝐴Q𝑥Q))
54simprd 112 . . . . 5 (𝐴 <Q 𝑥𝑥Q)
65adantr 270 . . . 4 ((𝐴 <Q 𝑥𝑥 <Q 𝐵) → 𝑥Q)
76pm4.71ri 384 . . 3 ((𝐴 <Q 𝑥𝑥 <Q 𝐵) ↔ (𝑥Q ∧ (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
87exbii 1537 . 2 (∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵) ↔ ∃𝑥(𝑥Q ∧ (𝐴 <Q 𝑥𝑥 <Q 𝐵)))
91, 2, 83bitr4i 210 1 (𝐴 <Q 𝐵 ↔ ∃𝑥(𝐴 <Q 𝑥𝑥 <Q 𝐵))
 Colors of variables: wff set class Syntax hints:   ∧ wa 102   ↔ wb 103  ∃wex 1422   ∈ wcel 1434  ∃wrex 2354   class class class wbr 3805  Qcnq 6584
 Copyright terms: Public domain W3C validator