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→∀zz<𝑸x→z∈C
9 1 ltexprlem4 ⊢B∈𝑷→x∈C→∃zz∈C∧x<𝑸z
10 df-rex ⊢∃z∈Cx<𝑸z↔∃zz∈C∧x<𝑸z
11 9 10 imbitrrdi ⊢B∈𝑷→x∈C→∃z∈Cx<𝑸z
12 8 11 jcad ⊢B∈𝑷→x∈C→∀zz<𝑸x→z∈C∧∃z∈Cx<𝑸z
13 12 ralrimiv ⊢B∈𝑷→∀x∈C∀zz<𝑸x→z∈C∧∃z∈Cx<𝑸z
14 13 adantr ⊢B∈𝑷∧A⊂B→∀x∈C∀zz<𝑸x→z∈C∧∃z∈Cx<𝑸z
15 elnp ⊢C∈𝑷↔∅⊂C∧C⊂𝑸∧∀x∈C∀zz<𝑸x→z∈C∧∃z∈Cx<𝑸z
16 5 7 14 15 syl21anbrc ⊢B∈𝑷∧A⊂B→C∈𝑷