Metamath Proof Explorer

Theorem ltexprlem7

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 ltexprlem7 ⊢A∈𝑷∧B∈𝑷∧A⊂B→B⊆A+𝑷C

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢C=x|∃y¬y∈A∧y+𝑸x∈B
2 1 ltexprlem5 ⊢B∈𝑷∧A⊂B→C∈𝑷
3 ltaddpr ⊢A∈𝑷∧C∈𝑷→A<𝑷A+𝑷C
4 addclpr ⊢A∈𝑷∧C∈𝑷→A+𝑷C∈𝑷
5 ltprord ⊢A∈𝑷∧A+𝑷C∈𝑷→A<𝑷A+𝑷C↔A⊂A+𝑷C
6 4 5 syldan ⊢A∈𝑷∧C∈𝑷→A<𝑷A+𝑷C↔A⊂A+𝑷C
7 3 6 mpbid ⊢A∈𝑷∧C∈𝑷→A⊂A+𝑷C
8 7 pssssd ⊢A∈𝑷∧C∈𝑷→A⊆A+𝑷C
9 8 sseld ⊢A∈𝑷∧C∈𝑷→w∈A→w∈A+𝑷C
10 9 2a1d ⊢A∈𝑷∧C∈𝑷→B∈𝑷→w∈B→w∈A→w∈A+𝑷C
11 10 com4r ⊢w∈A→A∈𝑷∧C∈𝑷→B∈𝑷→w∈B→w∈A+𝑷C
12 11 expd ⊢w∈A→A∈𝑷→C∈𝑷→B∈𝑷→w∈B→w∈A+𝑷C
13 prnmadd ⊢B∈𝑷∧w∈B→∃vw+𝑸v∈B
14 13 ex ⊢B∈𝑷→w∈B→∃vw+𝑸v∈B
15 elprnq ⊢B∈𝑷∧w+𝑸v∈B→w+𝑸v∈𝑸
16 addnqf ⊢+𝑸:𝑸×𝑸⟶𝑸
17 16 fdmi ⊢dom⁡+𝑸=𝑸×𝑸
18 0nnq ⊢¬∅∈𝑸
19 17 18 ndmovrcl ⊢w+𝑸v∈𝑸→w∈𝑸∧v∈𝑸
20 15 19 syl ⊢B∈𝑷∧w+𝑸v∈B→w∈𝑸∧v∈𝑸
21 20 simpld ⊢B∈𝑷∧w+𝑸v∈B→w∈𝑸
22 vex ⊢v∈V
23 22 prlem934 ⊢A∈𝑷→∃z∈A¬z+𝑸v∈A
24 23 adantr ⊢A∈𝑷∧C∈𝑷→∃z∈A¬z+𝑸v∈A
25 prub ⊢A∈𝑷∧z∈A∧w∈𝑸→¬w∈A→z<𝑸w
26 ltexnq ⊢w∈𝑸→z<𝑸w↔∃xz+𝑸x=w
27 26 adantl ⊢A∈𝑷∧z∈A∧w∈𝑸→z<𝑸w↔∃xz+𝑸x=w
28 25 27 sylibd ⊢A∈𝑷∧z∈A∧w∈𝑸→¬w∈A→∃xz+𝑸x=w
29 28 ex ⊢A∈𝑷∧z∈A→w∈𝑸→¬w∈A→∃xz+𝑸x=w
30 29 ad2ant2r ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A→w∈𝑸→¬w∈A→∃xz+𝑸x=w
31 vex ⊢z∈V
32 vex ⊢x∈V
33 addcomnq ⊢f+𝑸g=g+𝑸f
34 addassnq ⊢f+𝑸g+𝑸h=f+𝑸g+𝑸h
35 31 22 32 33 34 caov32 ⊢z+𝑸v+𝑸x=z+𝑸x+𝑸v
36 oveq1 ⊢z+𝑸x=w→z+𝑸x+𝑸v=w+𝑸v
37 35 36 eqtrid ⊢z+𝑸x=w→z+𝑸v+𝑸x=w+𝑸v
38 37 eleq1d ⊢z+𝑸x=w→z+𝑸v+𝑸x∈B↔w+𝑸v∈B
39 38 biimpar ⊢z+𝑸x=w∧w+𝑸v∈B→z+𝑸v+𝑸x∈B
40 ovex ⊢z+𝑸v∈V
41 eleq1 ⊢y=z+𝑸v→y∈A↔z+𝑸v∈A
42 41 notbid ⊢y=z+𝑸v→¬y∈A↔¬z+𝑸v∈A
43 oveq1 ⊢y=z+𝑸v→y+𝑸x=z+𝑸v+𝑸x
44 43 eleq1d ⊢y=z+𝑸v→y+𝑸x∈B↔z+𝑸v+𝑸x∈B
45 42 44 anbi12d ⊢y=z+𝑸v→¬y∈A∧y+𝑸x∈B↔¬z+𝑸v∈A∧z+𝑸v+𝑸x∈B
46 40 45 spcev ⊢¬z+𝑸v∈A∧z+𝑸v+𝑸x∈B→∃y¬y∈A∧y+𝑸x∈B
47 1 eqabri ⊢x∈C↔∃y¬y∈A∧y+𝑸x∈B
48 46 47 sylibr ⊢¬z+𝑸v∈A∧z+𝑸v+𝑸x∈B→x∈C
49 39 48 sylan2 ⊢¬z+𝑸v∈A∧z+𝑸x=w∧w+𝑸v∈B→x∈C
50 df-plp ⊢+𝑷=x∈𝑷,w∈𝑷⟼z|∃f∈x∃v∈wz=f+𝑸v
51 addclnq ⊢f∈𝑸∧v∈𝑸→f+𝑸v∈𝑸
52 50 51 genpprecl ⊢A∈𝑷∧C∈𝑷→z∈A∧x∈C→z+𝑸x∈A+𝑷C
53 49 52 sylan2i ⊢A∈𝑷∧C∈𝑷→z∈A∧¬z+𝑸v∈A∧z+𝑸x=w∧w+𝑸v∈B→z+𝑸x∈A+𝑷C
54 53 exp4d ⊢A∈𝑷∧C∈𝑷→z∈A→¬z+𝑸v∈A→z+𝑸x=w∧w+𝑸v∈B→z+𝑸x∈A+𝑷C
55 54 imp42 ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A∧z+𝑸x=w∧w+𝑸v∈B→z+𝑸x∈A+𝑷C
56 eleq1 ⊢z+𝑸x=w→z+𝑸x∈A+𝑷C↔w∈A+𝑷C
57 56 ad2antrl ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A∧z+𝑸x=w∧w+𝑸v∈B→z+𝑸x∈A+𝑷C↔w∈A+𝑷C
58 55 57 mpbid ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A∧z+𝑸x=w∧w+𝑸v∈B→w∈A+𝑷C
59 58 exp32 ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A→z+𝑸x=w→w+𝑸v∈B→w∈A+𝑷C
60 59 exlimdv ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A→∃xz+𝑸x=w→w+𝑸v∈B→w∈A+𝑷C
61 30 60 syl6d ⊢A∈𝑷∧C∈𝑷∧z∈A∧¬z+𝑸v∈A→w∈𝑸→¬w∈A→w+𝑸v∈B→w∈A+𝑷C
62 24 61 rexlimddv ⊢A∈𝑷∧C∈𝑷→w∈𝑸→¬w∈A→w+𝑸v∈B→w∈A+𝑷C
63 62 com14 ⊢w+𝑸v∈B→w∈𝑸→¬w∈A→A∈𝑷∧C∈𝑷→w∈A+𝑷C
64 63 adantl ⊢B∈𝑷∧w+𝑸v∈B→w∈𝑸→¬w∈A→A∈𝑷∧C∈𝑷→w∈A+𝑷C
65 21 64 mpd ⊢B∈𝑷∧w+𝑸v∈B→¬w∈A→A∈𝑷∧C∈𝑷→w∈A+𝑷C
66 65 ex ⊢B∈𝑷→w+𝑸v∈B→¬w∈A→A∈𝑷∧C∈𝑷→w∈A+𝑷C
67 66 exlimdv ⊢B∈𝑷→∃vw+𝑸v∈B→¬w∈A→A∈𝑷∧C∈𝑷→w∈A+𝑷C
68 14 67 syld ⊢B∈𝑷→w∈B→¬w∈A→A∈𝑷∧C∈𝑷→w∈A+𝑷C
69 68 com4t ⊢¬w∈A→A∈𝑷∧C∈𝑷→B∈𝑷→w∈B→w∈A+𝑷C
70 69 expd ⊢¬w∈A→A∈𝑷→C∈𝑷→B∈𝑷→w∈B→w∈A+𝑷C
71 12 70 pm2.61i ⊢A∈𝑷→C∈𝑷→B∈𝑷→w∈B→w∈A+𝑷C
72 2 71 syl5 ⊢A∈𝑷→B∈𝑷∧A⊂B→B∈𝑷→w∈B→w∈A+𝑷C
73 72 expd ⊢A∈𝑷→B∈𝑷→A⊂B→B∈𝑷→w∈B→w∈A+𝑷C
74 73 com34 ⊢A∈𝑷→B∈𝑷→B∈𝑷→A⊂B→w∈B→w∈A+𝑷C
75 74 pm2.43d ⊢A∈𝑷→B∈𝑷→A⊂B→w∈B→w∈A+𝑷C
76 75 imp31 ⊢A∈𝑷∧B∈𝑷∧A⊂B→w∈B→w∈A+𝑷C
77 76 ssrdv ⊢A∈𝑷∧B∈𝑷∧A⊂B→B⊆A+𝑷C