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

Theorem suplocexprlemml 7577
 Description: Lemma for suplocexpr 7586. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
Hypotheses
Ref Expression
suplocexpr.m (𝜑 → ∃𝑥 𝑥𝐴)
suplocexpr.ub (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
suplocexpr.loc (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
Assertion
Ref Expression
suplocexprlemml (𝜑 → ∃𝑠Q 𝑠 (1st𝐴))
Distinct variable groups:   𝐴,𝑠,𝑥,𝑦   𝜑,𝑠,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑧)   𝐴(𝑧)

Proof of Theorem suplocexprlemml
StepHypRef Expression
1 suplocexpr.m . . 3 (𝜑 → ∃𝑥 𝑥𝐴)
2 suplocexpr.ub . . . . . . 7 (𝜑 → ∃𝑥P𝑦𝐴 𝑦<P 𝑥)
3 suplocexpr.loc . . . . . . 7 (𝜑 → ∀𝑥P𝑦P (𝑥<P 𝑦 → (∃𝑧𝐴 𝑥<P 𝑧 ∨ ∀𝑧𝐴 𝑧<P 𝑦)))
41, 2, 3suplocexprlemss 7576 . . . . . 6 (𝜑𝐴P)
54sselda 3104 . . . . 5 ((𝜑𝑥𝐴) → 𝑥P)
6 prop 7336 . . . . 5 (𝑥P → ⟨(1st𝑥), (2nd𝑥)⟩ ∈ P)
7 prml 7338 . . . . 5 (⟨(1st𝑥), (2nd𝑥)⟩ ∈ P → ∃𝑠Q 𝑠 ∈ (1st𝑥))
85, 6, 73syl 17 . . . 4 ((𝜑𝑥𝐴) → ∃𝑠Q 𝑠 ∈ (1st𝑥))
98ralrimiva 2510 . . 3 (𝜑 → ∀𝑥𝐴𝑠Q 𝑠 ∈ (1st𝑥))
10 r19.2m 3456 . . 3 ((∃𝑥 𝑥𝐴 ∧ ∀𝑥𝐴𝑠Q 𝑠 ∈ (1st𝑥)) → ∃𝑥𝐴𝑠Q 𝑠 ∈ (1st𝑥))
111, 9, 10syl2anc 409 . 2 (𝜑 → ∃𝑥𝐴𝑠Q 𝑠 ∈ (1st𝑥))
12 suplocexprlemell 7574 . . . 4 (𝑠 (1st𝐴) ↔ ∃𝑥𝐴 𝑠 ∈ (1st𝑥))
1312rexbii 2447 . . 3 (∃𝑠Q 𝑠 (1st𝐴) ↔ ∃𝑠Q𝑥𝐴 𝑠 ∈ (1st𝑥))
14 rexcom 2600 . . 3 (∃𝑠Q𝑥𝐴 𝑠 ∈ (1st𝑥) ↔ ∃𝑥𝐴𝑠Q 𝑠 ∈ (1st𝑥))
1513, 14bitri 183 . 2 (∃𝑠Q 𝑠 (1st𝐴) ↔ ∃𝑥𝐴𝑠Q 𝑠 ∈ (1st𝑥))
1611, 15sylibr 133 1 (𝜑 → ∃𝑠Q 𝑠 (1st𝐴))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 698  ∃wex 1469   ∈ wcel 2112  ∀wral 2418  ∃wrex 2419  ⟨cop 3537  ∪ cuni 3746   class class class wbr 3939   “ cima 4554  ‘cfv 5135  1st c1st 6048  2nd c2nd 6049  Qcnq 7141  Pcnp 7152
 Copyright terms: Public domain W3C validator