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

Metamath Proof Explorer

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 eqabri ⊢ ( 𝑥 ∈ 𝐶 ↔ ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
13 12 exbii ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐶 ↔ ∃ 𝑥 ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
14 n0 ⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐶 )
15 excom ⊢ ( ∃ 𝑦 ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
16 13 14 15 3bitr4i ⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ( ¬ 𝑦 ∈ 𝐴 ∧ ( 𝑦 +Q 𝑥 ) ∈ 𝐵 ) )
17 11 16 imbitrrdi ⊢ ( 𝐵 ∈ P → ( 𝐴 ⊊ 𝐵 → 𝐶 ≠ ∅ ) )