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

Metamath Proof Explorer

Theorem xrsupexmnf

Description: Adding minus infinity to a set does not affect the existence of its supremum. (Contributed by NM, 26-Oct-2005)

Ref Expression
Assertion xrsupexmnf ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) 𝑦 < 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 elun ⊢ ( 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) ↔ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ { -∞ } ) )
2 simpr ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑥 < 𝑦 ) ) → ( 𝑦 ∈ 𝐴 → ¬ 𝑥 < 𝑦 ) )
3 velsn ⊢ ( 𝑦 ∈ { -∞ } ↔ 𝑦 = -∞ )
4 nltmnf ⊢ ( 𝑥 ∈ ℝ* → ¬ 𝑥 < -∞ )
5 breq2 ⊢ ( 𝑦 = -∞ → ( 𝑥 < 𝑦 ↔ 𝑥 < -∞ ) )
6 5 notbid ⊢ ( 𝑦 = -∞ → ( ¬ 𝑥 < 𝑦 ↔ ¬ 𝑥 < -∞ ) )
7 4 6 syl5ibrcom ⊢ ( 𝑥 ∈ ℝ* → ( 𝑦 = -∞ → ¬ 𝑥 < 𝑦 ) )
8 3 7 biimtrid ⊢ ( 𝑥 ∈ ℝ* → ( 𝑦 ∈ { -∞ } → ¬ 𝑥 < 𝑦 ) )
9 8 adantr ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑥 < 𝑦 ) ) → ( 𝑦 ∈ { -∞ } → ¬ 𝑥 < 𝑦 ) )
10 2 9 jaod ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑥 < 𝑦 ) ) → ( ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ { -∞ } ) → ¬ 𝑥 < 𝑦 ) )
11 1 10 biimtrid ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑥 < 𝑦 ) ) → ( 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) → ¬ 𝑥 < 𝑦 ) )
12 11 ex ⊢ ( 𝑥 ∈ ℝ* → ( ( 𝑦 ∈ 𝐴 → ¬ 𝑥 < 𝑦 ) → ( 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) → ¬ 𝑥 < 𝑦 ) ) )
13 12 ralimdv2 ⊢ ( 𝑥 ∈ ℝ* → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 → ∀ 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ) )
14 elun1 ⊢ ( 𝑧 ∈ 𝐴 → 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) )
15 14 anim1i ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑦 < 𝑧 ) → ( 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) ∧ 𝑦 < 𝑧 ) )
16 15 reximi2 ⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 → ∃ 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) 𝑦 < 𝑧 )
17 16 imim2i ⊢ ( ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) 𝑦 < 𝑧 ) )
18 17 ralimi ⊢ ( ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) → ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) 𝑦 < 𝑧 ) )
19 13 18 anim12d1 ⊢ ( 𝑥 ∈ ℝ* → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ( ∀ 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) 𝑦 < 𝑧 ) ) ) )
20 19 reximia ⊢ ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 < 𝑧 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∪ { -∞ } ) ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ ( 𝐴 ∪ { -∞ } ) 𝑦 < 𝑧 ) ) )