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