Metamath Proof Explorer

Theorem ltexprlem6

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 8-Apr-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢C=x|∃y¬y∈A∧y+𝑸x∈B
2 1 ltexprlem5 ⊢B∈𝑷∧A⊂B→C∈𝑷
3 df-plp ⊢+𝑷=z∈𝑷,y∈𝑷⟼f|∃g∈z∃h∈yf=g+𝑸h
4 addclnq ⊢g∈𝑸∧h∈𝑸→g+𝑸h∈𝑸
5 3 4 genpelv ⊢A∈𝑷∧C∈𝑷→z∈A+𝑷C↔∃w∈A∃x∈Cz=w+𝑸x
6 2 5 sylan2 ⊢A∈𝑷∧B∈𝑷∧A⊂B→z∈A+𝑷C↔∃w∈A∃x∈Cz=w+𝑸x
7 1 eqabri ⊢x∈C↔∃y¬y∈A∧y+𝑸x∈B
8 elprnq ⊢B∈𝑷∧y+𝑸x∈B→y+𝑸x∈𝑸
9 addnqf ⊢+𝑸:𝑸×𝑸⟶𝑸
10 9 fdmi ⊢dom⁡+𝑸=𝑸×𝑸
11 0nnq ⊢¬∅∈𝑸
12 10 11 ndmovrcl ⊢y+𝑸x∈𝑸→y∈𝑸∧x∈𝑸
13 12 simpld ⊢y+𝑸x∈𝑸→y∈𝑸
14 8 13 syl ⊢B∈𝑷∧y+𝑸x∈B→y∈𝑸
15 prub ⊢A∈𝑷∧w∈A∧y∈𝑸→¬y∈A→w<𝑸y
16 14 15 sylan2 ⊢A∈𝑷∧w∈A∧B∈𝑷∧y+𝑸x∈B→¬y∈A→w<𝑸y
17 12 simprd ⊢y+𝑸x∈𝑸→x∈𝑸
18 vex ⊢w∈V
19 vex ⊢y∈V
20 ltanq ⊢u∈𝑸→z<𝑸v↔u+𝑸z<𝑸u+𝑸v
21 vex ⊢x∈V
22 addcomnq ⊢z+𝑸v=v+𝑸z
23 18 19 20 21 22 caovord2 ⊢x∈𝑸→w<𝑸y↔w+𝑸x<𝑸y+𝑸x
24 8 17 23 3syl ⊢B∈𝑷∧y+𝑸x∈B→w<𝑸y↔w+𝑸x<𝑸y+𝑸x
25 prcdnq ⊢B∈𝑷∧y+𝑸x∈B→w+𝑸x<𝑸y+𝑸x→w+𝑸x∈B
26 24 25 sylbid ⊢B∈𝑷∧y+𝑸x∈B→w<𝑸y→w+𝑸x∈B
27 26 adantl ⊢A∈𝑷∧w∈A∧B∈𝑷∧y+𝑸x∈B→w<𝑸y→w+𝑸x∈B
28 16 27 syld ⊢A∈𝑷∧w∈A∧B∈𝑷∧y+𝑸x∈B→¬y∈A→w+𝑸x∈B
29 28 exp32 ⊢A∈𝑷∧w∈A→B∈𝑷→y+𝑸x∈B→¬y∈A→w+𝑸x∈B
30 29 com34 ⊢A∈𝑷∧w∈A→B∈𝑷→¬y∈A→y+𝑸x∈B→w+𝑸x∈B
31 30 imp4b ⊢A∈𝑷∧w∈A∧B∈𝑷→¬y∈A∧y+𝑸x∈B→w+𝑸x∈B
32 31 exlimdv ⊢A∈𝑷∧w∈A∧B∈𝑷→∃y¬y∈A∧y+𝑸x∈B→w+𝑸x∈B
33 7 32 biimtrid ⊢A∈𝑷∧w∈A∧B∈𝑷→x∈C→w+𝑸x∈B
34 33 exp31 ⊢A∈𝑷→w∈A→B∈𝑷→x∈C→w+𝑸x∈B
35 34 com23 ⊢A∈𝑷→B∈𝑷→w∈A→x∈C→w+𝑸x∈B
36 35 imp43 ⊢A∈𝑷∧B∈𝑷∧w∈A∧x∈C→w+𝑸x∈B
37 eleq1 ⊢z=w+𝑸x→z∈B↔w+𝑸x∈B
38 37 biimparc ⊢w+𝑸x∈B∧z=w+𝑸x→z∈B
39 36 38 sylan ⊢A∈𝑷∧B∈𝑷∧w∈A∧x∈C∧z=w+𝑸x→z∈B
40 39 exp31 ⊢A∈𝑷∧B∈𝑷→w∈A∧x∈C→z=w+𝑸x→z∈B
41 40 rexlimdvv ⊢A∈𝑷∧B∈𝑷→∃w∈A∃x∈Cz=w+𝑸x→z∈B
42 41 adantrr ⊢A∈𝑷∧B∈𝑷∧A⊂B→∃w∈A∃x∈Cz=w+𝑸x→z∈B
43 6 42 sylbid ⊢A∈𝑷∧B∈𝑷∧A⊂B→z∈A+𝑷C→z∈B
44 43 ssrdv ⊢A∈𝑷∧B∈𝑷∧A⊂B→A+𝑷C⊆B
45 44 anassrs ⊢A∈𝑷∧B∈𝑷∧A⊂B→A+𝑷C⊆B