This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 ) = 𝐵 )