Metamath Proof Explorer

Theorem ltexprlem3

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 ltexprlem3 ⊢B∈𝑷→x∈C→∀zz<𝑸x→z∈C

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢C=x|∃y¬y∈A∧y+𝑸x∈B
2 elprnq ⊢B∈𝑷∧y+𝑸x∈B→y+𝑸x∈𝑸
3 addnqf ⊢+𝑸:𝑸×𝑸⟶𝑸
4 3 fdmi ⊢dom⁡+𝑸=𝑸×𝑸
5 0nnq ⊢¬∅∈𝑸
6 4 5 ndmovrcl ⊢y+𝑸x∈𝑸→y∈𝑸∧x∈𝑸
7 6 simpld ⊢y+𝑸x∈𝑸→y∈𝑸
8 ltanq ⊢y∈𝑸→z<𝑸x↔y+𝑸z<𝑸y+𝑸x
9 2 7 8 3syl ⊢B∈𝑷∧y+𝑸x∈B→z<𝑸x↔y+𝑸z<𝑸y+𝑸x
10 prcdnq ⊢B∈𝑷∧y+𝑸x∈B→y+𝑸z<𝑸y+𝑸x→y+𝑸z∈B
11 9 10 sylbid ⊢B∈𝑷∧y+𝑸x∈B→z<𝑸x→y+𝑸z∈B
12 11 impancom ⊢B∈𝑷∧z<𝑸x→y+𝑸x∈B→y+𝑸z∈B
13 12 anim2d ⊢B∈𝑷∧z<𝑸x→¬y∈A∧y+𝑸x∈B→¬y∈A∧y+𝑸z∈B
14 13 eximdv ⊢B∈𝑷∧z<𝑸x→∃y¬y∈A∧y+𝑸x∈B→∃y¬y∈A∧y+𝑸z∈B
15 1 eqabri ⊢x∈C↔∃y¬y∈A∧y+𝑸x∈B
16 vex ⊢z∈V
17 oveq2 ⊢x=z→y+𝑸x=y+𝑸z
18 17 eleq1d ⊢x=z→y+𝑸x∈B↔y+𝑸z∈B
19 18 anbi2d ⊢x=z→¬y∈A∧y+𝑸x∈B↔¬y∈A∧y+𝑸z∈B
20 19 exbidv ⊢x=z→∃y¬y∈A∧y+𝑸x∈B↔∃y¬y∈A∧y+𝑸z∈B
21 16 20 1 elab2 ⊢z∈C↔∃y¬y∈A∧y+𝑸z∈B
22 14 15 21 3imtr4g ⊢B∈𝑷∧z<𝑸x→x∈C→z∈C
23 22 ex ⊢B∈𝑷→z<𝑸x→x∈C→z∈C
24 23 com23 ⊢B∈𝑷→x∈C→z<𝑸x→z∈C
25 24 alrimdv ⊢B∈𝑷→x∈C→∀zz<𝑸x→z∈C