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

Theorem ltexprlem5 10451
 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 . . . . 5 𝐶 = {𝑥 ∣ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}
21ltexprlem1 10447 . . . 4 (𝐵P → (𝐴𝐵𝐶 ≠ ∅))
3 0pss 4368 . . . 4 (∅ ⊊ 𝐶𝐶 ≠ ∅)
42, 3syl6ibr 255 . . 3 (𝐵P → (𝐴𝐵 → ∅ ⊊ 𝐶))
54imp 410 . 2 ((𝐵P𝐴𝐵) → ∅ ⊊ 𝐶)
61ltexprlem2 10448 . . 3 (𝐵P𝐶Q)
76adantr 484 . 2 ((𝐵P𝐴𝐵) → 𝐶Q)
81ltexprlem3 10449 . . . . 5 (𝐵P → (𝑥𝐶 → ∀𝑧(𝑧 <Q 𝑥𝑧𝐶)))
91ltexprlem4 10450 . . . . . 6 (𝐵P → (𝑥𝐶 → ∃𝑧(𝑧𝐶𝑥 <Q 𝑧)))
10 df-rex 3136 . . . . . 6 (∃𝑧𝐶 𝑥 <Q 𝑧 ↔ ∃𝑧(𝑧𝐶𝑥 <Q 𝑧))
119, 10syl6ibr 255 . . . . 5 (𝐵P → (𝑥𝐶 → ∃𝑧𝐶 𝑥 <Q 𝑧))
128, 11jcad 516 . . . 4 (𝐵P → (𝑥𝐶 → (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧)))
1312ralrimiv 3173 . . 3 (𝐵P → ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧))
1413adantr 484 . 2 ((𝐵P𝐴𝐵) → ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧))
15 elnp 10398 . 2 (𝐶P ↔ ((∅ ⊊ 𝐶𝐶Q) ∧ ∀𝑥𝐶 (∀𝑧(𝑧 <Q 𝑥𝑧𝐶) ∧ ∃𝑧𝐶 𝑥 <Q 𝑧)))
165, 7, 14, 15syl21anbrc 1341 1 ((𝐵P𝐴𝐵) → 𝐶P)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538  ∃wex 1781   ∈ wcel 2114  {cab 2800   ≠ wne 3011  ∀wral 3130  ∃wrex 3131   ⊊ wpss 3909  ∅c0 4265   class class class wbr 5042  (class class class)co 7140  Qcnq 10263   +Q cplq 10266
 Copyright terms: Public domain W3C validator