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	abeq2i	⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +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 𝑥 → 𝑧 ∈ 𝐶 ) ) )