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 syl5bi ( 𝑥 ∈ ℝ* → ( 𝑦 ∈ { +∞ } → ¬ 𝑦 < 𝑥 ) )
9 8 adantr ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦𝐴 → ¬ 𝑦 < 𝑥 ) ) → ( 𝑦 ∈ { +∞ } → ¬ 𝑦 < 𝑥 ) )
10 2 9 jaod ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦𝐴 → ¬ 𝑦 < 𝑥 ) ) → ( ( 𝑦𝐴𝑦 ∈ { +∞ } ) → ¬ 𝑦 < 𝑥 ) )
11 1 10 syl5bi ( ( 𝑥 ∈ ℝ* ∧ ( 𝑦𝐴 → ¬ 𝑦 < 𝑥 ) ) → ( 𝑦 ∈ ( 𝐴 ∪ { +∞ } ) → ¬ 𝑦 < 𝑥 ) )
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 ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∪ { +∞ } ) 𝑧 < 𝑦 ) ) )