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

Theorem prloc 6473
 Description: A Dedekind cut is located. (Contributed by Jim Kingdon, 23-Oct-2019.)
Assertion
Ref Expression
prloc ((⟨𝐿, 𝑈 P A <Q B) → (A 𝐿 B 𝑈))

Proof of Theorem prloc
Dummy variables 𝑞 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elinp 6456 . . . 4 (⟨𝐿, 𝑈 P ↔ (((𝐿Q 𝑈Q) (𝑞 Q 𝑞 𝐿 𝑟 Q 𝑟 𝑈)) ((𝑞 Q (𝑞 𝐿𝑟 Q (𝑞 <Q 𝑟 𝑟 𝐿)) 𝑟 Q (𝑟 𝑈𝑞 Q (𝑞 <Q 𝑟 𝑞 𝑈))) 𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))))
2 simpr3 911 . . . 4 ((((𝐿Q 𝑈Q) (𝑞 Q 𝑞 𝐿 𝑟 Q 𝑟 𝑈)) ((𝑞 Q (𝑞 𝐿𝑟 Q (𝑞 <Q 𝑟 𝑟 𝐿)) 𝑟 Q (𝑟 𝑈𝑞 Q (𝑞 <Q 𝑟 𝑞 𝑈))) 𝑞 Q ¬ (𝑞 𝐿 𝑞 𝑈) 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))
31, 2sylbi 114 . . 3 (⟨𝐿, 𝑈 P𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))
43adantr 261 . 2 ((⟨𝐿, 𝑈 P A <Q B) → 𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)))
5 simpr 103 . 2 ((⟨𝐿, 𝑈 P A <Q B) → A <Q B)
6 ltrelnq 6349 . . . . . . 7 <Q ⊆ (Q × Q)
76brel 4335 . . . . . 6 (A <Q B → (A Q B Q))
87simpld 105 . . . . 5 (A <Q BA Q)
98adantl 262 . . . 4 ((⟨𝐿, 𝑈 P A <Q B) → A Q)
10 simpr 103 . . . . . . 7 (((⟨𝐿, 𝑈 P A <Q B) 𝑞 = A) → 𝑞 = A)
1110breq1d 3765 . . . . . 6 (((⟨𝐿, 𝑈 P A <Q B) 𝑞 = A) → (𝑞 <Q 𝑟A <Q 𝑟))
1210eleq1d 2103 . . . . . . 7 (((⟨𝐿, 𝑈 P A <Q B) 𝑞 = A) → (𝑞 𝐿A 𝐿))
1312orbi1d 704 . . . . . 6 (((⟨𝐿, 𝑈 P A <Q B) 𝑞 = A) → ((𝑞 𝐿 𝑟 𝑈) ↔ (A 𝐿 𝑟 𝑈)))
1411, 13imbi12d 223 . . . . 5 (((⟨𝐿, 𝑈 P A <Q B) 𝑞 = A) → ((𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)) ↔ (A <Q 𝑟 → (A 𝐿 𝑟 𝑈))))
1514ralbidv 2320 . . . 4 (((⟨𝐿, 𝑈 P A <Q B) 𝑞 = A) → (𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)) ↔ 𝑟 Q (A <Q 𝑟 → (A 𝐿 𝑟 𝑈))))
169, 15rspcdv 2653 . . 3 ((⟨𝐿, 𝑈 P A <Q B) → (𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)) → 𝑟 Q (A <Q 𝑟 → (A 𝐿 𝑟 𝑈))))
177simprd 107 . . . . 5 (A <Q BB Q)
1817adantl 262 . . . 4 ((⟨𝐿, 𝑈 P A <Q B) → B Q)
19 simpr 103 . . . . . 6 (((⟨𝐿, 𝑈 P A <Q B) 𝑟 = B) → 𝑟 = B)
2019breq2d 3767 . . . . 5 (((⟨𝐿, 𝑈 P A <Q B) 𝑟 = B) → (A <Q 𝑟A <Q B))
2119eleq1d 2103 . . . . . 6 (((⟨𝐿, 𝑈 P A <Q B) 𝑟 = B) → (𝑟 𝑈B 𝑈))
2221orbi2d 703 . . . . 5 (((⟨𝐿, 𝑈 P A <Q B) 𝑟 = B) → ((A 𝐿 𝑟 𝑈) ↔ (A 𝐿 B 𝑈)))
2320, 22imbi12d 223 . . . 4 (((⟨𝐿, 𝑈 P A <Q B) 𝑟 = B) → ((A <Q 𝑟 → (A 𝐿 𝑟 𝑈)) ↔ (A <Q B → (A 𝐿 B 𝑈))))
2418, 23rspcdv 2653 . . 3 ((⟨𝐿, 𝑈 P A <Q B) → (𝑟 Q (A <Q 𝑟 → (A 𝐿 𝑟 𝑈)) → (A <Q B → (A 𝐿 B 𝑈))))
2516, 24syld 40 . 2 ((⟨𝐿, 𝑈 P A <Q B) → (𝑞 Q 𝑟 Q (𝑞 <Q 𝑟 → (𝑞 𝐿 𝑟 𝑈)) → (A <Q B → (A 𝐿 B 𝑈))))
264, 5, 25mp2d 41 1 ((⟨𝐿, 𝑈 P A <Q B) → (A 𝐿 B 𝑈))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 628   ∧ w3a 884   = wceq 1242   ∈ wcel 1390  ∀wral 2300  ∃wrex 2301   ⊆ wss 2911  ⟨cop 3370   class class class wbr 3755  Qcnq 6264
 Copyright terms: Public domain W3C validator