Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltexprlem5 Structured version   Visualization version   GIF version

Theorem ltexprlem5 9741
 Description: Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
Hypothesis
Ref Expression
ltexprlem.1 𝐶 = {𝑥 ∣ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}
Assertion
Ref Expression
ltexprlem5 ((𝐵P𝐴𝐵) → 𝐶P)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶
Allowed substitution hint:   𝐶(𝑦)

Proof of Theorem ltexprlem5
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 ltexprlem.1 . . . . . 6 𝐶 = {𝑥 ∣ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}
21ltexprlem1 9737 . . . . 5 (𝐵P → (𝐴𝐵𝐶 ≠ ∅))
3 0pss 3965 . . . . 5 (∅ ⊊ 𝐶𝐶 ≠ ∅)
42, 3syl6ibr 241 . . . 4 (𝐵P → (𝐴𝐵 → ∅ ⊊ 𝐶))
54imp 444 . . 3 ((𝐵P𝐴𝐵) → ∅ ⊊ 𝐶)
61ltexprlem2 9738 . . . 4 (𝐵P𝐶Q)
76adantr 480 . . 3 ((𝐵P𝐴𝐵) → 𝐶Q)
81ltexprlem3 9739 . . . . . 6 (𝐵P → (𝑥𝐶 → ∀𝑧(𝑧 <Q 𝑥𝑧𝐶)))
91ltexprlem4 9740 . . . . . . 7 (𝐵P → (𝑥𝐶 → ∃𝑧(𝑧𝐶𝑥 <Q 𝑧)))
10 df-rex 2902 . . . . . . 7 (∃𝑧𝐶 𝑥 <Q 𝑧 ↔ ∃𝑧(𝑧𝐶𝑥 <Q 𝑧))
119, 10syl6ibr 241 . . . . . 6 (𝐵P → (𝑥𝐶 → ∃𝑧𝐶 𝑥 <Q 𝑧))
128, 11jcad 554 . . . . 5 (𝐵P → (𝑥𝐶 → (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧)))
1312ralrimiv 2948 . . . 4 (𝐵P → ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧))
1413adantr 480 . . 3 ((𝐵P𝐴𝐵) → ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧))
155, 7, 14jca31 555 . 2 ((𝐵P𝐴𝐵) → ((∅ ⊊ 𝐶𝐶Q) ∧ ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧)))
16 elnp 9688 . 2 (𝐶P ↔ ((∅ ⊊ 𝐶𝐶Q) ∧ ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧)))
1715, 16sylibr 223 1 ((𝐵P𝐴𝐵) → 𝐶P)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ⊊ wpss 3541  ∅c0 3874   class class class wbr 4583  (class class class)co 6549  Qcnq 9553   +Q cplq 9556
 Copyright terms: Public domain W3C validator