Metamath Proof Explorer


Theorem ltexprlem5

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 6-Apr-1996) (New usage is discouraged.)

Ref Expression
Hypothesis ltexprlem.1 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
Assertion ltexprlem5 ( ( 𝐵P𝐴𝐵 ) → 𝐶P )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 1 ltexprlem1 ( 𝐵P → ( 𝐴𝐵𝐶 ≠ ∅ ) )
3 0pss ( ∅ ⊊ 𝐶𝐶 ≠ ∅ )
4 2 3 syl6ibr ( 𝐵P → ( 𝐴𝐵 → ∅ ⊊ 𝐶 ) )
5 4 imp ( ( 𝐵P𝐴𝐵 ) → ∅ ⊊ 𝐶 )
6 1 ltexprlem2 ( 𝐵P𝐶Q )
7 6 adantr ( ( 𝐵P𝐴𝐵 ) → 𝐶Q )
8 1 ltexprlem3 ( 𝐵P → ( 𝑥𝐶 → ∀ 𝑧 ( 𝑧 <Q 𝑥𝑧𝐶 ) ) )
9 1 ltexprlem4 ( 𝐵P → ( 𝑥𝐶 → ∃ 𝑧 ( 𝑧𝐶𝑥 <Q 𝑧 ) ) )
10 df-rex ( ∃ 𝑧𝐶 𝑥 <Q 𝑧 ↔ ∃ 𝑧 ( 𝑧𝐶𝑥 <Q 𝑧 ) )
11 9 10 syl6ibr ( 𝐵P → ( 𝑥𝐶 → ∃ 𝑧𝐶 𝑥 <Q 𝑧 ) )
12 8 11 jcad ( 𝐵P → ( 𝑥𝐶 → ( ∀ 𝑧 ( 𝑧 <Q 𝑥𝑧𝐶 ) ∧ ∃ 𝑧𝐶 𝑥 <Q 𝑧 ) ) )
13 12 ralrimiv ( 𝐵P → ∀ 𝑥𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥𝑧𝐶 ) ∧ ∃ 𝑧𝐶 𝑥 <Q 𝑧 ) )
14 13 adantr ( ( 𝐵P𝐴𝐵 ) → ∀ 𝑥𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥𝑧𝐶 ) ∧ ∃ 𝑧𝐶 𝑥 <Q 𝑧 ) )
15 elnp ( 𝐶P ↔ ( ( ∅ ⊊ 𝐶𝐶Q ) ∧ ∀ 𝑥𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥𝑧𝐶 ) ∧ ∃ 𝑧𝐶 𝑥 <Q 𝑧 ) ) )
16 5 7 14 15 syl21anbrc ( ( 𝐵P𝐴𝐵 ) → 𝐶P )