Theorem ltexpri

Description: Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 13-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	ltexpri	⊢ ( 𝐴 <P 𝐵 → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	⊢ <P ⊆ ( P × P )
2	1	brel	⊢ ( 𝐴 <P 𝐵 → ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) )
3		ltprord	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 <P 𝐵 ↔ 𝐴 ⊊ 𝐵 ) )
4		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑤 +Q 𝑦 ) = ( 𝑤 +Q 𝑧 ) )
5	4	eleq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ↔ ( 𝑤 +Q 𝑧 ) ∈ 𝐵 ) )
6	5	anbi2d	⊢ ( 𝑦 = 𝑧 → ( ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) ↔ ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑧 ) ∈ 𝐵 ) ) )
7	6	exbidv	⊢ ( 𝑦 = 𝑧 → ( ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) ↔ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑧 ) ∈ 𝐵 ) ) )
8	7	cbvabv	⊢ { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } = { 𝑧 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑧 ) ∈ 𝐵 ) }
9	8	ltexprlem5	⊢ ( ( 𝐵 ∈ P ∧ 𝐴 ⊊ 𝐵 ) → { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ∈ P )
10	9	adantll	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ∈ P )
11	8	ltexprlem6	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐴 +P { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ) ⊆ 𝐵 )
12	8	ltexprlem7	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → 𝐵 ⊆ ( 𝐴 +P { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ) )
13	11 12	eqssd	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → ( 𝐴 +P { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ) = 𝐵 )
14		oveq2	⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } → ( 𝐴 +P 𝑥 ) = ( 𝐴 +P { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ) )
15	14	eqeq1d	⊢ ( 𝑥 = { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } → ( ( 𝐴 +P 𝑥 ) = 𝐵 ↔ ( 𝐴 +P { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ) = 𝐵 ) )
16	15	rspcev	⊢ ( ( { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ∈ P ∧ ( 𝐴 +P { 𝑦 ∣ ∃ 𝑤 ( ¬ 𝑤 ∈ 𝐴 ∧ ( 𝑤 +Q 𝑦 ) ∈ 𝐵 ) } ) = 𝐵 ) → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 )
17	10 13 16	syl2anc	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ 𝐴 ⊊ 𝐵 ) → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 )
18	17	ex	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 ) )
19	3 18	sylbid	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 <P 𝐵 → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 ) )
20	2 19	mpcom	⊢ ( 𝐴 <P 𝐵 → ∃ 𝑥 ∈ P ( 𝐴 +P 𝑥 ) = 𝐵 )