Metamath Proof Explorer

Theorem ltexprlem4

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

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 prnmax ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑤 ∈ 𝐵 ( 𝑦 +Q 𝑥 ) <Q 𝑤 )
3 df-rex ⊢ ( ∃ 𝑤 ∈ 𝐵 ( 𝑦 +Q 𝑥 ) <Q 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) )
4 2 3 sylib ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) )
5 ltrelnq ⊢ <Q ⊆ ( Q × Q )
6 5 brel ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → ( ( 𝑦 +Q 𝑥 ) ∈ Q ∧ 𝑤 ∈ Q ) )
7 6 simpld ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → ( 𝑦 +Q 𝑥 ) ∈ Q )
8 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
9 8 fdmi ⊢ dom +Q = ( Q × Q )
10 0nnq ⊢ ¬ ∅ ∈ Q
11 9 10 ndmovrcl ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) )
12 7 11 syl ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) )
13 ltaddnq ⊢ ( ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) → 𝑦 <Q ( 𝑦 +Q 𝑥 ) )
14 ltsonq ⊢ <Q Or Q
15 14 5 sotri ⊢ ( ( 𝑦 <Q ( 𝑦 +Q 𝑥 ) ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → 𝑦 <Q 𝑤 )
16 13 15 sylan ⊢ ( ( ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → 𝑦 <Q 𝑤 )
17 12 16 mpancom ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → 𝑦 <Q 𝑤 )
18 5 brel ⊢ ( 𝑦 <Q 𝑤 → ( 𝑦 ∈ Q ∧ 𝑤 ∈ Q ) )
19 18 simprd ⊢ ( 𝑦 <Q 𝑤 → 𝑤 ∈ Q )
20 ltexnq ⊢ ( 𝑤 ∈ Q → ( 𝑦 <Q 𝑤 ↔ ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = 𝑤 ) )
21 20 biimpd ⊢ ( 𝑤 ∈ Q → ( 𝑦 <Q 𝑤 → ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = 𝑤 ) )
22 19 21 mpcom ⊢ ( 𝑦 <Q 𝑤 → ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = 𝑤 )
23 17 22 syl ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = 𝑤 )
24 eqcom ⊢ ( 𝑤 = ( 𝑦 +Q 𝑧 ) ↔ ( 𝑦 +Q 𝑧 ) = 𝑤 )
25 24 exbii ⊢ ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ↔ ∃ 𝑧 ( 𝑦 +Q 𝑧 ) = 𝑤 )
26 23 25 sylibr ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) )
27 26 ancri ⊢ ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 → ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) )
28 27 anim2i ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → ( 𝑤 ∈ 𝐵 ∧ ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
29 an12 ⊢ ( ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) ↔ ( 𝑤 ∈ 𝐵 ∧ ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
30 28 29 sylibr ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
31 19.41v ⊢ ( ∃ 𝑧 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) ↔ ( ∃ 𝑧 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
32 30 31 sylibr ⊢ ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → ∃ 𝑧 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
33 32 eximi ⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → ∃ 𝑤 ∃ 𝑧 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
34 excom ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) ↔ ∃ 𝑤 ∃ 𝑧 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
35 33 34 sylibr ⊢ ( ∃ 𝑤 ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) → ∃ 𝑧 ∃ 𝑤 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) )
36 ovex ⊢ ( 𝑦 +Q 𝑧 ) ∈ V
37 eleq1 ⊢ ( 𝑤 = ( 𝑦 +Q 𝑧 ) → ( 𝑤 ∈ 𝐵 ↔ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
38 breq2 ⊢ ( 𝑤 = ( 𝑦 +Q 𝑧 ) → ( ( 𝑦 +Q 𝑥 ) <Q 𝑤 ↔ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑧 ) ) )
39 37 38 anbi12d ⊢ ( 𝑤 = ( 𝑦 +Q 𝑧 ) → ( ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ↔ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑧 ) ) ) )
40 36 39 ceqsexv ⊢ ( ∃ 𝑤 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) ↔ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑧 ) ) )
41 ltanq ⊢ ( 𝑦 ∈ Q → ( 𝑥 <Q 𝑧 ↔ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑧 ) ) )
42 9 5 10 41 ndmovordi ⊢ ( ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑧 ) → 𝑥 <Q 𝑧 )
43 42 anim2i ⊢ ( ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q ( 𝑦 +Q 𝑧 ) ) → ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) )
44 40 43 sylbi ⊢ ( ∃ 𝑤 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) → ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) )
45 44 eximi ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝑤 = ( 𝑦 +Q 𝑧 ) ∧ ( 𝑤 ∈ 𝐵 ∧ ( 𝑦 +Q 𝑥 ) <Q 𝑤 ) ) → ∃ 𝑧 ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) )
46 4 35 45 3syl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑧 ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) )
47 46 anim2i ⊢ ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) → ( ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑧 ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
48 47 an12s ⊢ ( ( 𝐵 ∈ P ∧ ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) → ( ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑧 ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
49 19.42v ⊢ ( ∃ 𝑧 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) ↔ ( ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑧 ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
50 48 49 sylibr ⊢ ( ( 𝐵 ∈ P ∧ ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) → ∃ 𝑧 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
51 50 ex ⊢ ( 𝐵 ∈ P → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑧 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) ) )
52 51 eximdv ⊢ ( 𝐵 ∈ P → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ∃ 𝑧 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) ) )
53 1 abeq2i ⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
54 vex ⊢ 𝑧 ∈ V
55 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 +Q 𝑥 ) = ( 𝑦 +Q 𝑧 ) )
56 55 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ↔ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
57 56 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ) )
58 57 exbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ) )
59 54 58 1 elab2 ⊢ ( 𝑧 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
60 59 anbi1i ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ↔ ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ∧ 𝑥 <Q 𝑧 ) )
61 19.41v ⊢ ( ∃ 𝑦 ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ∧ 𝑥 <Q 𝑧 ) ↔ ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ∧ 𝑥 <Q 𝑧 ) )
62 anass ⊢ ( ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ∧ 𝑥 <Q 𝑧 ) ↔ ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
63 62 exbii ⊢ ( ∃ 𝑦 ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ∧ 𝑥 <Q 𝑧 ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
64 60 61 63 3bitr2i ⊢ ( ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
65 64 exbii ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ↔ ∃ 𝑧 ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
66 excom ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) ↔ ∃ 𝑧 ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
67 65 66 bitr4i ⊢ ( ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ↔ ∃ 𝑦 ∃ 𝑧 ( ¬ 𝑦 ∈ 𝐴 ∧ ( ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ∧ 𝑥 <Q 𝑧 ) ) )
68 52 53 67 3imtr4g ⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ) )