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 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
Assertion ltexprlem7 ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → 𝐵 ⊆ ( 𝐴 +P 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 1 ltexprlem5 ⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ∈ P )
3 ltaddpr ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝐴 <P ( 𝐴 +P 𝐶 ) )
4 addclpr ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 +P 𝐶 ) ∈ P )
5 ltprord ⊢ ( ( 𝐴 ∈ P ∧ ( 𝐴 +P 𝐶 ) ∈ P ) → ( 𝐴 <P ( 𝐴 +P 𝐶 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐶 ) ) )
6 4 5 syldan ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 <P ( 𝐴 +P 𝐶 ) ↔ 𝐴 ⊊ ( 𝐴 +P 𝐶 ) ) )
7 3 6 mpbid ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝐴 ⊊ ( 𝐴 +P 𝐶 ) )
8 7 pssssd ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝐴 ⊆ ( 𝐴 +P 𝐶 ) )
9 8 sseld ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
10 9 2a1d ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
11 10 com4r ⊢ ( 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
12 11 expd ⊢ ( 𝑤 ∈ 𝐴 → ( 𝐴 ∈ P → ( 𝐶 ∈ P → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
13 prnmadd ⊢ ( ( 𝐵 ∈ P ∧ 𝑤 ∈ 𝐵 ) → ∃ 𝑣 ( 𝑤 +Q 𝑣 ) ∈ 𝐵 )
14 13 ex ⊢ ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → ∃ 𝑣 ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) )
15 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑤 +Q 𝑣 ) ∈ Q )
16 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
17 16 fdmi ⊢ dom +Q = ( Q × Q )
18 0nnq ⊢ ¬ ∅ ∈ Q
19 17 18 ndmovrcl ⊢ ( ( 𝑤 +Q 𝑣 ) ∈ Q → ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) )
20 15 19 syl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑤 ∈ Q ∧ 𝑣 ∈ Q ) )
21 20 simpld ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → 𝑤 ∈ Q )
22 vex ⊢ 𝑣 ∈ V
23 22 prlem934 ⊢ ( 𝐴 ∈ P → ∃ 𝑧 ∈ 𝐴 ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 )
24 23 adantr ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ∃ 𝑧 ∈ 𝐴 ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 )
25 prub ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( ¬ 𝑤 ∈ 𝐴 → 𝑧 <Q 𝑤 ) )
26 ltexnq ⊢ ( 𝑤 ∈ Q → ( 𝑧 <Q 𝑤 ↔ ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) )
27 26 adantl ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( 𝑧 <Q 𝑤 ↔ ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) )
28 25 27 sylibd ⊢ ( ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑤 ∈ Q ) → ( ¬ 𝑤 ∈ 𝐴 → ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) )
29 28 ex ⊢ ( ( 𝐴 ∈ P ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 ∈ Q → ( ¬ 𝑤 ∈ 𝐴 → ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) ) )
30 29 ad2ant2r ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( 𝑤 ∈ Q → ( ¬ 𝑤 ∈ 𝐴 → ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 ) ) )
31 vex ⊢ 𝑧 ∈ V
32 vex ⊢ 𝑥 ∈ V
33 addcomnq ⊢ ( 𝑓 +Q 𝑔 ) = ( 𝑔 +Q 𝑓 )
34 addassnq ⊢ ( ( 𝑓 +Q 𝑔 ) +Q ℎ ) = ( 𝑓 +Q ( 𝑔 +Q ℎ ) )
35 31 22 32 33 34 caov32 ⊢ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) = ( ( 𝑧 +Q 𝑥 ) +Q 𝑣 )
36 oveq1 ⊢ ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑧 +Q 𝑥 ) +Q 𝑣 ) = ( 𝑤 +Q 𝑣 ) )
37 35 36 syl5eq ⊢ ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) = ( 𝑤 +Q 𝑣 ) )
38 37 eleq1d ⊢ ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ↔ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) )
39 38 biimpar ⊢ ( ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 )
40 ovex ⊢ ( 𝑧 +Q 𝑣 ) ∈ V
41 eleq1 ⊢ ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( 𝑦 ∈ 𝐴 ↔ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) )
42 41 notbid ⊢ ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( ¬ 𝑦 ∈ 𝐴 ↔ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) )
43 oveq1 ⊢ ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( 𝑦 +Q 𝑥 ) = ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) )
44 43 eleq1d ⊢ ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ↔ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) )
45 42 44 anbi12d ⊢ ( 𝑦 = ( 𝑧 +Q 𝑣 ) → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) ) )
46 40 45 spcev ⊢ ( ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
47 1 abeq2i ⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
48 46 47 sylibr ⊢ ( ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑣 ) +Q 𝑥 ) ∈ 𝐵 ) → 𝑥 ∈ 𝐶 )
49 39 48 sylan2 ⊢ ( ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → 𝑥 ∈ 𝐶 )
50 df-plp ⊢ +P = ( 𝑥 ∈ P , 𝑤 ∈ P ↦ { 𝑧 ∣ ∃ 𝑓 ∈ 𝑥 ∃ 𝑣 ∈ 𝑤 𝑧 = ( 𝑓 +Q 𝑣 ) } )
51 addclnq ⊢ ( ( 𝑓 ∈ Q ∧ 𝑣 ∈ Q ) → ( 𝑓 +Q 𝑣 ) ∈ Q )
52 50 51 genpprecl ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑧 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶 ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ) )
53 49 52 sylan2i ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝑧 ∈ 𝐴 ∧ ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ) )
54 53 exp4d ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑧 ∈ 𝐴 → ( ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 → ( ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
55 54 imp42 ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) )
56 eleq1 ⊢ ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ↔ 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
57 56 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → ( ( 𝑧 +Q 𝑥 ) ∈ ( 𝐴 +P 𝐶 ) ↔ 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
58 55 57 mpbid ⊢ ( ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) ∧ ( ( 𝑧 +Q 𝑥 ) = 𝑤 ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) )
59 58 exp32 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) )
60 59 exlimdv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( ∃ 𝑥 ( 𝑧 +Q 𝑥 ) = 𝑤 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) )
61 30 60 syl6d ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ ( 𝑧 +Q 𝑣 ) ∈ 𝐴 ) ) → ( 𝑤 ∈ Q → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
62 24 61 rexlimddv ⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝑤 ∈ Q → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
63 62 com14 ⊢ ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → ( 𝑤 ∈ Q → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
64 63 adantl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( 𝑤 ∈ Q → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
65 21 64 mpd ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑤 +Q 𝑣 ) ∈ 𝐵 ) → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) )
66 65 ex ⊢ ( 𝐵 ∈ P → ( ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
67 66 exlimdv ⊢ ( 𝐵 ∈ P → ( ∃ 𝑣 ( 𝑤 +Q 𝑣 ) ∈ 𝐵 → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
68 14 67 syld ⊢ ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
69 68 com4t ⊢ ( ¬ 𝑤 ∈ 𝐴 → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
70 69 expd ⊢ ( ¬ 𝑤 ∈ 𝐴 → ( 𝐴 ∈ P → ( 𝐶 ∈ P → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
71 12 70 pm2.61i ⊢ ( 𝐴 ∈ P → ( 𝐶 ∈ P → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
72 2 71 syl5 ⊢ ( 𝐴 ∈ P → ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
73 72 expd ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → ( 𝐵 ∈ P → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
74 73 com34 ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) ) )
75 74 pm2.43d ⊢ ( 𝐴 ∈ P → ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) ) ) )
76 75 imp31 ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → ( 𝑤 ∈ 𝐵 → 𝑤 ∈ ( 𝐴 +P 𝐶 ) ) )
77 76 ssrdv ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → 𝐵 ⊆ ( 𝐴 +P 𝐶 ) )