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

Theorem nqprdisj 6642
 Description: A cut produced from a rational is disjoint. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.)
Assertion
Ref Expression
nqprdisj (𝐴Q → ∀𝑞Q ¬ (𝑞 ∈ {𝑥𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥𝐴 <Q 𝑥}))
Distinct variable group:   𝑥,𝐴,𝑞

Proof of Theorem nqprdisj
StepHypRef Expression
1 ltsonq 6496 . . . . 5 <Q Or Q
2 ltrelnq 6463 . . . . 5 <Q ⊆ (Q × Q)
31, 2son2lpi 4721 . . . 4 ¬ (𝑞 <Q 𝐴𝐴 <Q 𝑞)
4 vex 2560 . . . . . 6 𝑞 ∈ V
5 breq1 3767 . . . . . 6 (𝑥 = 𝑞 → (𝑥 <Q 𝐴𝑞 <Q 𝐴))
64, 5elab 2687 . . . . 5 (𝑞 ∈ {𝑥𝑥 <Q 𝐴} ↔ 𝑞 <Q 𝐴)
7 breq2 3768 . . . . . 6 (𝑥 = 𝑞 → (𝐴 <Q 𝑥𝐴 <Q 𝑞))
84, 7elab 2687 . . . . 5 (𝑞 ∈ {𝑥𝐴 <Q 𝑥} ↔ 𝐴 <Q 𝑞)
96, 8anbi12i 433 . . . 4 ((𝑞 ∈ {𝑥𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥𝐴 <Q 𝑥}) ↔ (𝑞 <Q 𝐴𝐴 <Q 𝑞))
103, 9mtbir 596 . . 3 ¬ (𝑞 ∈ {𝑥𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥𝐴 <Q 𝑥})
1110rgenw 2376 . 2 𝑞Q ¬ (𝑞 ∈ {𝑥𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥𝐴 <Q 𝑥})
1211a1i 9 1 (𝐴Q → ∀𝑞Q ¬ (𝑞 ∈ {𝑥𝑥 <Q 𝐴} ∧ 𝑞 ∈ {𝑥𝐴 <Q 𝑥}))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∈ wcel 1393  {cab 2026  ∀wral 2306   class class class wbr 3764  Qcnq 6378
 Copyright terms: Public domain W3C validator