limsupval3

Description: The superior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupval3.1	⊢ Ⅎ 𝑘 𝜑
	limsupval3.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	limsupval3.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ^* )
	limsupval3.4	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ^* , < ) )
Assertion	limsupval3	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		limsupval3.1	⊢ Ⅎ 𝑘 𝜑
2		limsupval3.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		limsupval3.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℝ^* )
4		limsupval3.4	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ^* , < ) )
5	3 2	fexd	⊢ ( 𝜑 → 𝐹 ∈ V )
6		eqid	⊢ ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
7	6	limsupval	⊢ ( 𝐹 ∈ V → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
8	5 7	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) )
9	4	a1i	⊢ ( 𝜑 → 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ^* , < ) ) )
10	3	fimassd	⊢ ( 𝜑 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ^* )
11		dfss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ⊆ ℝ^* ↔ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
12	10 11	sylib	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) = ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
13	12	eqcomd	⊢ ( 𝜑 → ( 𝐹 “ ( 𝑘 [,) +∞ ) ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) )
14	13	supeq1d	⊢ ( 𝜑 → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ^* , < ) = sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℝ ) → sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ^* , < ) = sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
16	1 15	mpteq2da	⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ sup ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) , ℝ^* , < ) ) = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) )
17	9 16	eqtr2d	⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = 𝐺 )
18	17	rneqd	⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) = ran 𝐺 )
19	18	infeq1d	⊢ ( 𝜑 → inf ( ran ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ) , ℝ^* , < ) = inf ( ran 𝐺 , ℝ^* , < ) )
20	8 19	eqtrd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem limsupval3

Proof