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

Metamath Proof Explorer

Theorem infmremnf

Description: The infimum of the reals is minus infinity. (Contributed by AV, 5-Sep-2020)

		Ref	Expression
	Assertion	infmremnf	⊢ inf ( ℝ , ℝ^* , < ) = -∞

Proof

Step	Hyp	Ref	Expression
1		reltxrnmnf	⊢ ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 )
2		xrltso	⊢ < Or ℝ^*
3	2	a1i	⊢ ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) → < Or ℝ^* )
4		mnfxr	⊢ -∞ ∈ ℝ^*
5	4	a1i	⊢ ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) → -∞ ∈ ℝ^* )
6		rexr	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ^* )
7		nltmnf	⊢ ( 𝑦 ∈ ℝ^* → ¬ 𝑦 < -∞ )
8	6 7	syl	⊢ ( 𝑦 ∈ ℝ → ¬ 𝑦 < -∞ )
9	8	adantl	⊢ ( ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) ∧ 𝑦 ∈ ℝ ) → ¬ 𝑦 < -∞ )
10		breq2	⊢ ( 𝑥 = 𝑦 → ( -∞ < 𝑥 ↔ -∞ < 𝑦 ) )
11		breq2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 < 𝑥 ↔ 𝑧 < 𝑦 ) )
12	11	rexbidv	⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ↔ ∃ 𝑧 ∈ ℝ 𝑧 < 𝑦 ) )
13	10 12	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) ↔ ( -∞ < 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑦 ) ) )
14	13	rspcv	⊢ ( 𝑦 ∈ ℝ^* → ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) → ( -∞ < 𝑦 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑦 ) ) )
15	14	com23	⊢ ( 𝑦 ∈ ℝ^* → ( -∞ < 𝑦 → ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑦 ) ) )
16	15	imp	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -∞ < 𝑦 ) → ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑦 ) )
17	16	impcom	⊢ ( ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) ∧ ( 𝑦 ∈ ℝ^* ∧ -∞ < 𝑦 ) ) → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑦 )
18	3 5 9 17	eqinfd	⊢ ( ∀ 𝑥 ∈ ℝ^* ( -∞ < 𝑥 → ∃ 𝑧 ∈ ℝ 𝑧 < 𝑥 ) → inf ( ℝ , ℝ^* , < ) = -∞ )
19	1 18	ax-mp	⊢ inf ( ℝ , ℝ^* , < ) = -∞