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	⊢ ( ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ ( 𝐴 ∪ { +∞ } ) ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ ( 𝐴 ∪ { +∞ } ) 𝑧 < 𝑦 ) ) )