This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 imbitrrdi ⊢ ( 𝐵 ∈ 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 imbitrrdi ⊢ ( 𝐵 ∈ 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 )