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 → ∃ v w + 𝑸 v ∈ B
14 13 ex ⊢ B ∈ 𝑷 → w ∈ B → ∃ v w + 𝑸 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 ↔ ∃ x z + 𝑸 x = w
27 26 adantl ⊢ A ∈ 𝑷 ∧ z ∈ A ∧ w ∈ 𝑸 → z < 𝑸 w ↔ ∃ x z + 𝑸 x = w
28 25 27 sylibd ⊢ A ∈ 𝑷 ∧ z ∈ A ∧ w ∈ 𝑸 → ¬ w ∈ A → ∃ x z + 𝑸 x = w
29 28 ex ⊢ A ∈ 𝑷 ∧ z ∈ A → w ∈ 𝑸 → ¬ w ∈ A → ∃ x z + 𝑸 x = w
30 29 ad2ant2r ⊢ A ∈ 𝑷 ∧ C ∈ 𝑷 ∧ z ∈ A ∧ ¬ z + 𝑸 v ∈ A → w ∈ 𝑸 → ¬ w ∈ A → ∃ x z + 𝑸 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 syl5eq ⊢ 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 abeq2i ⊢ 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 ∈ w z = 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 → ∃ x z + 𝑸 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 ∈ 𝑷 → ∃ v w + 𝑸 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