Theorem liminfresxr

Description: The inferior limit of a function only depends on the preimage of the extended real part. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfresxr.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	liminfresxr.2	⊢ ( 𝜑 → Fun 𝐹 )
	liminfresxr.3	⊢ 𝐴 = ( ◡ 𝐹 “ ℝ* )
Assertion	liminfresxr	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝐴 ) ) = ( lim inf ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		liminfresxr.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
2		liminfresxr.2	⊢ ( 𝜑 → Fun 𝐹 )
3		liminfresxr.3	⊢ 𝐴 = ( ◡ 𝐹 “ ℝ* )
4		resimass	⊢ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) )
5	4	a1i	⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ⊆ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
6	5	ssrind	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
7	2	funfnd	⊢ ( 𝜑 → 𝐹 Fn dom 𝐹 )
8		elinel1	⊢ ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) )
9		fvelima2	⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝑦 ∈ ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ) → ∃ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑥 ) = 𝑦 )
10	7 8 9	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ∃ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑥 ) = 𝑦 )
11		elinel1	⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) → 𝑥 ∈ dom 𝐹 )
12	11	3ad2ant2	⊢ ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ dom 𝐹 )
13		simpr	⊢ ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
14		elinel2	⊢ ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) → 𝑦 ∈ ℝ* )
15	14	adantr	⊢ ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ ℝ* )
16	13 15	eqeltrd	⊢ ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
17	16	3adant2	⊢ ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
18	12 17	jca	⊢ ( ( 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) )
19	18	3adant1l	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) )
20		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝜑 )
21		elpreima	⊢ ( 𝐹 Fn dom 𝐹 → ( 𝑥 ∈ ( ◡ 𝐹 “ ℝ* ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) ) )
22	7 21	syl	⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ ℝ* ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) ) )
23	20 22	syl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ℝ* ) ↔ ( 𝑥 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ) ) )
24	19 23	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ ( ◡ 𝐹 “ ℝ* ) )
25	24 3	eleqtrrdi	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ 𝐴 )
26	25	3expa	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ 𝐴 )
27	26	fvresd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
28		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = 𝑦 )
29	27 28	eqtr2d	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 = ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) )
30		simplll	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝜑 )
31	2	funresd	⊢ ( 𝜑 → Fun ( 𝐹 ↾ 𝐴 ) )
32	30 31	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → Fun ( 𝐹 ↾ 𝐴 ) )
33	11	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ dom 𝐹 )
34	26 33	elind	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ ( 𝐴 ∩ dom 𝐹 ) )
35		dmres	⊢ dom ( 𝐹 ↾ 𝐴 ) = ( 𝐴 ∩ dom 𝐹 )
36	34 35	eleqtrrdi	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) )
37	32 36	jca	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) )
38		elinel2	⊢ ( 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) → 𝑥 ∈ ( 𝑘 [,) +∞ ) )
39	38	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑥 ∈ ( 𝑘 [,) +∞ ) )
40		funfvima	⊢ ( ( Fun ( 𝐹 ↾ 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐹 ↾ 𝐴 ) ) → ( 𝑥 ∈ ( 𝑘 [,) +∞ ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ) )
41	37 39 40	sylc	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → ( ( 𝐹 ↾ 𝐴 ) ‘ 𝑥 ) ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
42	29 41	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) ∧ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝑦 ) → 𝑦 ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
43	42	rexlimdva2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → ( ∃ 𝑥 ∈ ( dom 𝐹 ∩ ( 𝑘 [,) +∞ ) ) ( 𝐹 ‘ 𝑥 ) = 𝑦 → 𝑦 ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ) )
44	10 43	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ) → 𝑦 ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
45	44	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑦 ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
46		dfss3	⊢ ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ↔ ∀ 𝑦 ∈ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) 𝑦 ∈ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
47	45 46	sylibr	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) )
48		inss2	⊢ ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ*
49	48	a1i	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ℝ* )
50	47 49	ssind	⊢ ( 𝜑 → ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) ⊆ ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
51	6 50	eqssd	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) = ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) )
52	51	infeq1d	⊢ ( 𝜑 → inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) = inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
53	52	mpteq2dv	⊢ ( 𝜑 → ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
54	53	rneqd	⊢ ( 𝜑 → ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) )
55	54	supeq1d	⊢ ( 𝜑 → sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
56	1	resexd	⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ V )
57		eqid	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
58	57	liminfval	⊢ ( ( 𝐹 ↾ 𝐴 ) ∈ V → ( lim inf ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
59	56 58	syl	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝐴 ) ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( ( 𝐹 ↾ 𝐴 ) “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
60		eqid	⊢ ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) = ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) )
61	60	liminfval	⊢ ( 𝐹 ∈ 𝑉 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
62	1 61	syl	⊢ ( 𝜑 → ( lim inf ‘ 𝐹 ) = sup ( ran ( 𝑘 ∈ ℝ ↦ inf ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ* ) , ℝ* , < ) ) , ℝ* , < ) )
63	55 59 62	3eqtr4d	⊢ ( 𝜑 → ( lim inf ‘ ( 𝐹 ↾ 𝐴 ) ) = ( lim inf ‘ 𝐹 ) )