Theorem ltexprlem5

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	ltexprlem5	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ∈ P )

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2	1	ltexprlem1	⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅ ) )
3		0pss	⊢ ( ∅ ⊊ 𝐶 ↔ 𝐶 ≠ ∅ )
4	2 3	imbitrrdi	⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → ∅ ⊊ 𝐶 ) )
5	4	imp	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → ∅ ⊊ 𝐶 )
6	1	ltexprlem2	⊢ ( 𝐵 ∈ P → 𝐶 ⊊ Q )
7	6	adantr	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ⊊ Q )
8	1	ltexprlem3	⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ) )
9	1	ltexprlem4	⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) ) )
10		df-rex	⊢ ( ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ↔ ∃ 𝑧 ( 𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧 ) )
11	9 10	imbitrrdi	⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) )
12	8 11	jcad	⊢ ( 𝐵 ∈ P → ( 𝑥 ∈ 𝐶 → ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) )
13	12	ralrimiv	⊢ ( 𝐵 ∈ P → ∀ 𝑥 ∈ 𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) )
14	13	adantr	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → ∀ 𝑥 ∈ 𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) )
15		elnp	⊢ ( 𝐶 ∈ P ↔ ( ( ∅ ⊊ 𝐶 ∧ 𝐶 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐶 ( ∀ 𝑧 ( 𝑧 <Q 𝑥 → 𝑧 ∈ 𝐶 ) ∧ ∃ 𝑧 ∈ 𝐶 𝑥 <Q 𝑧 ) ) )
16	5 7 14 15	syl21anbrc	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → 𝐶 ∈ P )