This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ltexprlem3

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 ltexprlem3 ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑦 +Q 𝑥 ) ∈ Q )
3 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
4 3 fdmi ⊢ dom +Q = ( Q × Q )
5 0nnq ⊢ ¬ ∅ ∈ Q
6 4 5 ndmovrcl ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) )
7 6 simpld ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → 𝑦 ∈ Q )
8 ltanq ⊢ ( 𝑦 ∈ Q → ( 𝑧 <Q 𝑥 ↔ ( 𝑦 +Q 𝑧 ) <Q ( 𝑦 +Q 𝑥 ) ) )
9 2 7 8 3syl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑧 <Q 𝑥 ↔ ( 𝑦 +Q 𝑧 ) <Q ( 𝑦 +Q 𝑥 ) ) )
10 prcdnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( ( 𝑦 +Q 𝑧 ) <Q ( 𝑦 +Q 𝑥 ) → ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
11 9 10 sylbid ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑧 <Q 𝑥 → ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
12 11 impancom ⊢ ( ( 𝐵 ∈ P ∧ 𝑧 <Q 𝑥 ) → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 → ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
13 12 anim2d ⊢ ( ( 𝐵 ∈ P ∧ 𝑧 <Q 𝑥 ) → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ) )
14 13 eximdv ⊢ ( ( 𝐵 ∈ P ∧ 𝑧 <Q 𝑥 ) → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ) )
15 1 eqabri ⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
16 vex ⊢ 𝑧 ∈ V
17 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 +Q 𝑥 ) = ( 𝑦 +Q 𝑧 ) )
18 17 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ↔ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
19 18 anbi2d ⊢ ( 𝑥 = 𝑧 → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ) )
20 19 exbidv ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) ) )
21 16 20 1 elab2 ⊢ ( 𝑧 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑧 ) ∈ 𝐵 ) )
22 14 15 21 3imtr4g ⊢ ( ( 𝐵 ∈ P ∧ 𝑧 <Q 𝑥 ) → ( 𝑥 ∈ 𝐶 → 𝑧 ∈ 𝐶 ) )
23 22 ex ⊢ ( 𝐵 ∈ P → ( 𝑧 <Q 𝑥 → ( 𝑥 ∈ 𝐶 → 𝑧 ∈ 𝐶 ) ) )
24 23 com23 ⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ) )
25 24 alrimdv ⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ) )