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	abeq2i	⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +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	syl5bi	⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐵 ) )
20	19	ssrdv	⊢ ( 𝐵 ∈ P → 𝐶 ⊆ 𝐵 )
21		prpssnq	⊢ ( 𝐵 ∈ P → 𝐵 ⊊ Q )
22	20 21	sspsstrd	⊢ ( 𝐵 ∈ P → 𝐶 ⊊ Q )