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→∃yy∈B∧¬y∈A
3 prnmadd ⊢B∈𝑷∧y∈B→∃xy+𝑸x∈B
4 3 anim2i ⊢¬y∈A∧B∈𝑷∧y∈B→¬y∈A∧∃xy+𝑸x∈B
5 19.42v ⊢∃x¬y∈A∧y+𝑸x∈B↔¬y∈A∧∃xy+𝑸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∈𝑷→∃yy∈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 ⊢∃xx∈C↔∃x∃y¬y∈A∧y+𝑸x∈B
14 n0 ⊢C≠∅↔∃xx∈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≠∅