Theorem ltexprlem1

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	ltexprlem1	⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		ltexprlem.1	⊢ 𝐶 = { 𝑥 ∣ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) }
2		pssnel	⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐴 ) )
3		prnmadd	⊢ ( ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ( 𝑦 +Q 𝑥 ) ∈ 𝐵 )
4	3	anim2i	⊢ ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) ) → ( ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
5		19.42v	⊢ ( ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ( ¬ 𝑦 ∈ 𝐴 ∧ ∃ 𝑥 ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
6	4 5	sylibr	⊢ ( ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝐵 ∈ P ∧ 𝑦 ∈ 𝐵 ) ) → ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
7	6	exp32	⊢ ( ¬ 𝑦 ∈ 𝐴 → ( 𝐵 ∈ P → ( 𝑦 ∈ 𝐵 → ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) ) )
8	7	com3l	⊢ ( 𝐵 ∈ P → ( 𝑦 ∈ 𝐵 → ( ¬ 𝑦 ∈ 𝐴 → ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) ) )
9	8	impd	⊢ ( 𝐵 ∈ P → ( ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) )
10	9	eximdv	⊢ ( 𝐵 ∈ P → ( ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ ¬ 𝑦 ∈ 𝐴 ) → ∃ 𝑦 ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) )
11	2 10	syl5	⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → ∃ 𝑦 ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ) )
12	1	abeq2i	⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
13	12	exbii	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐶 ↔ ∃ 𝑥 ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
14		n0	⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐶 )
15		excom	⊢ ( ∃ 𝑦 ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
16	13 14 15	3bitr4i	⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
17	11 16	syl6ibr	⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅ ) )