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

Metamath Proof Explorer

Theorem xrinfmexpnf

Description: Adding plus infinity to a set does not affect the existence of its infimum. (Contributed by NM, 19-Jan-2006)

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

Proof

Step Hyp Ref Expression
1 elun ⊢ ( 𝑦 ∈ ( 𝐴 ∪ { +∞ } ) ↔ ( 𝑦 ∈ 𝐴 ∨ 𝑦 ∈ { +∞ } ) )
2 simpr ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥 ) ) → ( 𝑦 ∈ 𝐴 → ¬ 𝑦 < 𝑥 ) )
3 velsn ⊢ ( 𝑦 ∈ { +∞ } ↔ 𝑦 = +∞ )
4 pnfnlt ⊢ ( 𝑥 ∈ ℝ* → ¬ +∞ < 𝑥 )
5 breq1 ⊢ ( 𝑦 = +∞ → ( 𝑦 < 𝑥 ↔ +∞ < 𝑥 ) )
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 ⊢ ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∪ { +∞ } ) 𝑧 < 𝑦 ) ) )