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

Metamath Proof Explorer

Theorem ltexprlem2

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 3-Apr-1996) (New usage is discouraged.)

Ref Expression
Hypothesis ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
Assertion ltexprlem2 ( 𝐵 ∈ P → 𝐶 ⊊ Q )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2 1 eqabri ⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
3 elprnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑦 +Q 𝑥 ) ∈ Q )
4 addnqf ⊢ +Q : ( Q × Q ) ⟶ Q
5 4 fdmi ⊢ dom +Q = ( Q × Q )
6 0nnq ⊢ ¬ ∅ ∈ Q
7 5 6 ndmovrcl ⊢ ( ( 𝑦 +Q 𝑥 ) ∈ Q → ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) )
8 3 7 syl ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) )
9 ltaddnq ⊢ ( ( 𝑥 ∈ Q ∧ 𝑦 ∈ Q ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) )
10 9 ancoms ⊢ ( ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) → 𝑥 <Q ( 𝑥 +Q 𝑦 ) )
11 addcomnq ⊢ ( 𝑥 +Q 𝑦 ) = ( 𝑦 +Q 𝑥 )
12 10 11 breqtrdi ⊢ ( ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) → 𝑥 <Q ( 𝑦 +Q 𝑥 ) )
13 prcdnq ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( 𝑥 <Q ( 𝑦 +Q 𝑥 ) → 𝑥 ∈ 𝐵 ) )
14 12 13 syl5 ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → ( ( 𝑦 ∈ Q ∧ 𝑥 ∈ Q ) → 𝑥 ∈ 𝐵 ) )
15 8 14 mpd ⊢ ( ( 𝐵 ∈ P ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
16 15 ex ⊢ ( 𝐵 ∈ P → ( ( 𝑦 +Q 𝑥 ) ∈ 𝐵 → 𝑥 ∈ 𝐵 ) )
17 16 adantld ⊢ ( 𝐵 ∈ P → ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) )
18 17 exlimdv ⊢ ( 𝐵 ∈ P → ( ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) )
19 2 18 biimtrid ⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) )
20 19 ssrdv ⊢ ( 𝐵 ∈ P → 𝐶 ⊆ 𝐵 )
21 prpssnq ⊢ ( 𝐵 ∈ P → 𝐵 ⊊ Q )
22 20 21 sspsstrd ⊢ ( 𝐵 ∈ P → 𝐶 ⊊ Q )