Metamath Proof Explorer

Theorem ltexprlem1

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

Ref Expression
Hypothesis ltexprlem.1 ⊢ C = x | ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
Assertion ltexprlem1 ⊢ B ∈ 𝑷 → A ⊂ B → C ≠ ∅

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ C = x | ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
2 pssnel ⊢ A ⊂ B → ∃ y y ∈ B ∧ ¬ y ∈ A
3 prnmadd ⊢ B ∈ 𝑷 ∧ y ∈ B → ∃ x y + 𝑸 x ∈ B
4 3 anim2i ⊢ ¬ y ∈ A ∧ B ∈ 𝑷 ∧ y ∈ B → ¬ y ∈ A ∧ ∃ x y + 𝑸 x ∈ B
5 19.42v ⊢ ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B ↔ ¬ y ∈ A ∧ ∃ x y + 𝑸 x ∈ B
6 4 5 sylibr ⊢ ¬ y ∈ A ∧ B ∈ 𝑷 ∧ y ∈ B → ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
7 6 exp32 ⊢ ¬ y ∈ A → B ∈ 𝑷 → y ∈ B → ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
8 7 com3l ⊢ B ∈ 𝑷 → y ∈ B → ¬ y ∈ A → ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
9 8 impd ⊢ B ∈ 𝑷 → y ∈ B ∧ ¬ y ∈ A → ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
10 9 eximdv ⊢ B ∈ 𝑷 → ∃ y y ∈ B ∧ ¬ y ∈ A → ∃ y ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
11 2 10 syl5 ⊢ B ∈ 𝑷 → A ⊂ B → ∃ y ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
12 1 eqabri ⊢ x ∈ C ↔ ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
13 12 exbii ⊢ ∃ x x ∈ C ↔ ∃ x ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
14 n0 ⊢ C ≠ ∅ ↔ ∃ x x ∈ C
15 excom ⊢ ∃ y ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B ↔ ∃ x ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
16 13 14 15 3bitr4i ⊢ C ≠ ∅ ↔ ∃ y ∃ x ¬ y ∈ A ∧ y + 𝑸 x ∈ B
17 11 16 imbitrrdi ⊢ B ∈ 𝑷 → A ⊂ B → C ≠ ∅