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

Metamath Proof Explorer

Theorem liminfval

Description: The inferior limit of a set F . (Contributed by Glauco Siliprandi, 2-Jan-2022)

		Ref	Expression
	Hypothesis	liminfval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
	Assertion	liminfval	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		liminfval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
2		df-liminf	⊢ lim inf = ( 𝑥 ∈ V ↦ sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
3		imaeq1	⊢ ( 𝑥 = 𝐹 → ( 𝑥 “ ( 𝑘 [,) +∞ ) ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
4	3	ineq1d	⊢ ( 𝑥 = 𝐹 → ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) )
5	4	infeq1d	⊢ ( 𝑥 = 𝐹 → inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
6	5	mpteq2dv	⊢ ( 𝑥 = 𝐹 → ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
7	1	a1i	⊢ ( 𝑥 = 𝐹 → 𝐺 = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
8	6 7	eqtr4d	⊢ ( 𝑥 = 𝐹 → ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = 𝐺 )
9	8	rneqd	⊢ ( 𝑥 = 𝐹 → ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ran 𝐺 )
10	9	supeq1d	⊢ ( 𝑥 = 𝐹 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝑥 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) = sup ( ran 𝐺 , ℝ^* , < ) )
11		elex	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 ∈ V )
12		xrltso	⊢ < Or ℝ^*
13	12	supex	⊢ sup ( ran 𝐺 , ℝ^* , < ) ∈ V
14	13	a1i	⊢ ( 𝐹 ∈ 𝑉 → sup ( ran 𝐺 , ℝ^* , < ) ∈ V )
15	2 10 11 14	fvmptd3	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran 𝐺 , ℝ^* , < ) )