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

Theorem prdisj 6340
 Description: A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.)
Assertion
Ref Expression
prdisj ((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈))

Proof of Theorem prdisj
Dummy variables 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2078 . . . . 5 (𝑞 = A → (𝑞 QA Q))
21anbi2d 440 . . . 4 (𝑞 = A → ((⟨𝐿, 𝑈 P 𝑞 Q) ↔ (⟨𝐿, 𝑈 P A Q)))
3 eleq1 2078 . . . . . 6 (𝑞 = A → (𝑞 𝐿A 𝐿))
4 eleq1 2078 . . . . . 6 (𝑞 = A → (𝑞 𝑈A 𝑈))
53, 4anbi12d 445 . . . . 5 (𝑞 = A → ((𝑞 𝐿 𝑞 𝑈) ↔ (A 𝐿 A 𝑈)))
65notbid 579 . . . 4 (𝑞 = A → (¬ (𝑞 𝐿 𝑞 𝑈) ↔ ¬ (A 𝐿 A 𝑈)))
72, 6imbi12d 223 . . 3 (𝑞 = A → (((⟨𝐿, 𝑈 P 𝑞 Q) → ¬ (𝑞 𝐿 𝑞 𝑈)) ↔ ((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈))))
8 elinp 6322 . . . . 5 (⟨𝐿, 𝑈 P ↔ (((𝐿Q 𝑈Q) (𝑞 Q 𝑞 𝐿 𝑟 Q 𝑟 𝑈)) ((𝑞 Q (𝑞 𝐿𝑟 Q (𝑞 <Q 𝑟 𝑟 𝐿)) 𝑟 Q (𝑟 𝑈𝑞 Q (𝑞 <Q 𝑟 𝑞 𝑈))) 𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))))
9 simpr2 897 . . . . 5 ((((𝐿Q 𝑈Q) (𝑞 Q 𝑞 𝐿 𝑟 Q 𝑟 𝑈)) ((𝑞 Q (𝑞 𝐿𝑟 Q (𝑞 <Q 𝑟 𝑟 𝐿)) 𝑟 Q (𝑟 𝑈𝑞 Q (𝑞 <Q 𝑟 𝑞 𝑈))) 𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))) → 𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈))
108, 9sylbi 114 . . . 4 (⟨𝐿, 𝑈 P𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈))
1110r19.21bi 2381 . . 3 ((⟨𝐿, 𝑈 P 𝑞 Q) → ¬ (𝑞 𝐿 𝑞 𝑈))
127, 11vtoclg 2586 . 2 (A Q → ((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈)))
1312anabsi7 502 1 ((⟨𝐿, 𝑈 P A Q) → ¬ (A 𝐿 A 𝑈))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 871   = wceq 1226   ∈ wcel 1370  ∀wral 2280  ∃wrex 2281   ⊆ wss 2890  ⟨cop 3349   class class class wbr 3734  Qcnq 6134
 Copyright terms: Public domain W3C validator