Theorem limsupgle

Description: The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

	Ref	Expression
Hypothesis	limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
Assertion	limsupgle	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐺 ‘ 𝐶 ) ≤ 𝐴 ↔ ∀ 𝑗 ∈ 𝐵 ( 𝐶 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
2	1	limsupgval	⊢ ( 𝐶 ∈ ℝ → ( 𝐺 ‘ 𝐶 ) = sup ( ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
3	2	3ad2ant2	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( 𝐺 ‘ 𝐶 ) = sup ( ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
4	3	breq1d	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐺 ‘ 𝐶 ) ≤ 𝐴 ↔ sup ( ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝐴 ) )
5		inss2	⊢ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
6		simp3	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → 𝐴 ∈ ℝ* )
7		supxrleub	⊢ ( ( ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( sup ( ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝐴 ) )
8	5 6 7	sylancr	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( sup ( ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝐴 ) )
9		imassrn	⊢ ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ⊆ ran 𝐹
10		simp1r	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → 𝐹 : 𝐵 ⟶ ℝ* )
11	10	frnd	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ran 𝐹 ⊆ ℝ* )
12	9 11	sstrid	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ⊆ ℝ* )
13		df-ss	⊢ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ⊆ ℝ* ↔ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝐶 [,) +∞ ) ) )
14	12 13	sylib	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ ( 𝐶 [,) +∞ ) ) )
15		imadmres	⊢ ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ) = ( 𝐹 “ ( 𝐶 [,) +∞ ) )
16	14 15	eqtr4di	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) = ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ) )
17	16	raleqdv	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝐴 ↔ ∀ 𝑥 ∈ ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ) 𝑥 ≤ 𝐴 ) )
18	10	ffnd	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → 𝐹 Fn 𝐵 )
19	10	fdmd	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → dom 𝐹 = 𝐵 )
20	19	ineq2d	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐶 [,) +∞ ) ∩ dom 𝐹 ) = ( ( 𝐶 [,) +∞ ) ∩ 𝐵 ) )
21		dmres	⊢ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) = ( ( 𝐶 [,) +∞ ) ∩ dom 𝐹 )
22		incom	⊢ ( 𝐵 ∩ ( 𝐶 [,) +∞ ) ) = ( ( 𝐶 [,) +∞ ) ∩ 𝐵 )
23	20 21 22	3eqtr4g	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) = ( 𝐵 ∩ ( 𝐶 [,) +∞ ) ) )
24		inss1	⊢ ( 𝐵 ∩ ( 𝐶 [,) +∞ ) ) ⊆ 𝐵
25	23 24	eqsstrdi	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ⊆ 𝐵 )
26		breq1	⊢ ( 𝑥 = ( 𝐹 ‘ 𝑗 ) → ( 𝑥 ≤ 𝐴 ↔ ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
27	26	ralima	⊢ ( ( 𝐹 Fn 𝐵 ∧ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ) 𝑥 ≤ 𝐴 ↔ ∀ 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
28	18 25 27	syl2anc	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ( 𝐹 “ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ) 𝑥 ≤ 𝐴 ↔ ∀ 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) )
29	23	eleq2d	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ↔ 𝑗 ∈ ( 𝐵 ∩ ( 𝐶 [,) +∞ ) ) ) )
30		elin	⊢ ( 𝑗 ∈ ( 𝐵 ∩ ( 𝐶 [,) +∞ ) ) ↔ ( 𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ( 𝐶 [,) +∞ ) ) )
31	29 30	bitrdi	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ↔ ( 𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ( 𝐶 [,) +∞ ) ) ) )
32		simpl2	⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) ∧ 𝑗 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
33		simp1l	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → 𝐵 ⊆ ℝ )
34	33	sselda	⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) ∧ 𝑗 ∈ 𝐵 ) → 𝑗 ∈ ℝ )
35		elicopnf	⊢ ( 𝐶 ∈ ℝ → ( 𝑗 ∈ ( 𝐶 [,) +∞ ) ↔ ( 𝑗 ∈ ℝ ∧ 𝐶 ≤ 𝑗 ) ) )
36	35	baibd	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑗 ∈ ℝ ) → ( 𝑗 ∈ ( 𝐶 [,) +∞ ) ↔ 𝐶 ≤ 𝑗 ) )
37	32 34 36	syl2anc	⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) ∧ 𝑗 ∈ 𝐵 ) → ( 𝑗 ∈ ( 𝐶 [,) +∞ ) ↔ 𝐶 ≤ 𝑗 ) )
38	37	pm5.32da	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ( 𝐶 [,) +∞ ) ) ↔ ( 𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗 ) ) )
39	31 38	bitrd	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ↔ ( 𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗 ) ) )
40	39	imbi1d	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( ( 𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
41		impexp	⊢ ( ( ( 𝑗 ∈ 𝐵 ∧ 𝐶 ≤ 𝑗 ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( 𝑗 ∈ 𝐵 → ( 𝐶 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
42	40 41	bitrdi	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ↔ ( 𝑗 ∈ 𝐵 → ( 𝐶 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) ) )
43	42	ralbidv2	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ∀ 𝑗 ∈ dom ( 𝐹 ↾ ( 𝐶 [,) +∞ ) ) ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ↔ ∀ 𝑗 ∈ 𝐵 ( 𝐶 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
44	17 28 43	3bitrd	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ∀ 𝑥 ∈ ( ( 𝐹 “ ( 𝐶 [,) +∞ ) ) ∩ ℝ* ) 𝑥 ≤ 𝐴 ↔ ∀ 𝑗 ∈ 𝐵 ( 𝐶 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )
45	4 8 44	3bitrd	⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝐹 : 𝐵 ⟶ ℝ* ) ∧ 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ* ) → ( ( 𝐺 ‘ 𝐶 ) ≤ 𝐴 ↔ ∀ 𝑗 ∈ 𝐵 ( 𝐶 ≤ 𝑗 → ( 𝐹 ‘ 𝑗 ) ≤ 𝐴 ) ) )