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 ⊢ C = x | ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
Assertion ltexprlem5 ⊢ B ∈ 𝑷 ∧ A ⊂ B → C ∈ 𝑷

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ C = x | ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
2 1 ltexprlem1 ⊢ B ∈ 𝑷 → A ⊂ B → C ≠ ∅
3 0pss ⊢ ∅ ⊂ C ↔ C ≠ ∅
4 2 3 imbitrrdi ⊢ B ∈ 𝑷 → A ⊂ B → ∅ ⊂ C
5 4 imp ⊢ B ∈ 𝑷 ∧ A ⊂ B → ∅ ⊂ C
6 1 ltexprlem2 ⊢ B ∈ 𝑷 → C ⊂ 𝑸
7 6 adantr ⊢ B ∈ 𝑷 ∧ A ⊂ B → C ⊂ 𝑸
8 1 ltexprlem3 ⊢ B ∈ 𝑷 → x ∈ C → ∀ z z < 𝑸 x → z ∈ C
9 1 ltexprlem4 ⊢ B ∈ 𝑷 → x ∈ C → ∃ z z ∈ C ∧ x < 𝑸 z
10 df-rex ⊢ ∃ z ∈ C x < 𝑸 z ↔ ∃ z z ∈ C ∧ x < 𝑸 z
11 9 10 imbitrrdi ⊢ B ∈ 𝑷 → x ∈ C → ∃ z ∈ C x < 𝑸 z
12 8 11 jcad ⊢ B ∈ 𝑷 → x ∈ C → ∀ z z < 𝑸 x → z ∈ C ∧ ∃ z ∈ C x < 𝑸 z
13 12 ralrimiv ⊢ B ∈ 𝑷 → ∀ x ∈ C ∀ z z < 𝑸 x → z ∈ C ∧ ∃ z ∈ C x < 𝑸 z
14 13 adantr ⊢ B ∈ 𝑷 ∧ A ⊂ B → ∀ x ∈ C ∀ z z < 𝑸 x → z ∈ C ∧ ∃ z ∈ C x < 𝑸 z
15 elnp ⊢ C ∈ 𝑷 ↔ ∅ ⊂ C ∧ C ⊂ 𝑸 ∧ ∀ x ∈ C ∀ z z < 𝑸 x → z ∈ C ∧ ∃ z ∈ C x < 𝑸 z
16 5 7 14 15 syl21anbrc ⊢ B ∈ 𝑷 ∧ A ⊂ B → C ∈ 𝑷