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	$⊢ φ \to F \in V$
	liminfresxr.2	$⊢ φ \to Fun F$
	liminfresxr.3	$⊢ A = F^{-1} [ℝ^{*}]$
Assertion	liminfresxr	$⊢ φ \to lim inf ({F ↾}_{A}) = lim inf (F)$

Proof

Step	Hyp	Ref	Expression
1		liminfresxr.1	$⊢ φ \to F \in V$
2		liminfresxr.2	$⊢ φ \to Fun F$
3		liminfresxr.3	$⊢ A = F^{-1} [ℝ^{*}]$
4		resimass	$⊢ ({F ↾}_{A}) [[k, +∞)] \subseteq F [[k, +∞)]$
5	4	a1i	$⊢ φ \to ({F ↾}_{A}) [[k, +∞)] \subseteq F [[k, +∞)]$
6	5	ssrind	$⊢ φ \to ({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} \subseteq F [[k, +∞)] \cap ℝ^{}$
7	2	funfnd	$⊢ φ \to F Fn dom F$
8		elinel1	$⊢ y \in (F [[k, +∞)] \cap ℝ^{*}) \to y \in F [[k, +∞)]$
9		fvelima2	$⊢ (F Fn dom F \land y \in F [[k, +∞)]) \to \exists x \in (dom F \cap [k, +∞)) F (x) = y$
10	7 8 9	syl2an	$⊢ (φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \to \exists x \in (dom F \cap [k, +∞)) F (x) = y$
11		elinel1	$⊢ x \in (dom F \cap [k, +∞)) \to x \in dom F$
12	11	3ad2ant2	$⊢ (y \in (F [[k, +∞)] \cap ℝ^{*}) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to x \in dom F$
13		simpr	$⊢ (y \in (F [[k, +∞)] \cap ℝ^{*}) \land F (x) = y) \to F (x) = y$
14		elinel2	$⊢ y \in (F [[k, +∞)] \cap ℝ^{}) \to y \in ℝ^{}$
15	14	adantr	$⊢ (y \in (F [[k, +∞)] \cap ℝ^{}) \land F (x) = y) \to y \in ℝ^{}$
16	13 15	eqeltrd	$⊢ (y \in (F [[k, +∞)] \cap ℝ^{}) \land F (x) = y) \to F (x) \in ℝ^{}$
17	16	3adant2	$⊢ (y \in (F [[k, +∞)] \cap ℝ^{}) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to F (x) \in ℝ^{}$
18	12 17	jca	$⊢ (y \in (F [[k, +∞)] \cap ℝ^{}) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to (x \in dom F \land F (x) \in ℝ^{})$
19	18	3adant1l	$⊢ ((φ \land y \in (F [[k, +∞)] \cap ℝ^{})) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to (x \in dom F \land F (x) \in ℝ^{})$
20		simp1l	$⊢ ((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to φ$
21		elpreima	$⊢ F Fn dom F \to (x \in F^{-1} [ℝ^{}] \leftrightarrow (x \in dom F \land F (x) \in ℝ^{}))$
22	7 21	syl	$⊢ φ \to (x \in F^{-1} [ℝ^{}] \leftrightarrow (x \in dom F \land F (x) \in ℝ^{}))$
23	20 22	syl	$⊢ ((φ \land y \in (F [[k, +∞)] \cap ℝ^{})) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to (x \in F^{-1} [ℝ^{}] \leftrightarrow (x \in dom F \land F (x) \in ℝ^{*}))$
24	19 23	mpbird	$⊢ ((φ \land y \in (F [[k, +∞)] \cap ℝ^{})) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to x \in F^{-1} [ℝ^{}]$
25	24 3	eleqtrrdi	$⊢ ((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞)) \land F (x) = y) \to x \in A$
26	25	3expa	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to x \in A$
27	26	fvresd	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to ({F ↾}_{A}) (x) = F (x)$
28		simpr	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to F (x) = y$
29	27 28	eqtr2d	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to y = ({F ↾}_{A}) (x)$
30		simplll	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to φ$
31	2	funresd	$⊢ φ \to Fun ({F ↾}_{A})$
32	30 31	syl	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to Fun ({F ↾}_{A})$
33	11	ad2antlr	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to x \in dom F$
34	26 33	elind	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to x \in (A \cap dom F)$
35		dmres	$⊢ dom ({F ↾}_{A}) = A \cap dom F$
36	34 35	eleqtrrdi	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to x \in dom ({F ↾}_{A})$
37	32 36	jca	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to (Fun ({F ↾}_{A}) \land x \in dom ({F ↾}_{A}))$
38		elinel2	$⊢ x \in (dom F \cap [k, +∞)) \to x \in [k, +∞)$
39	38	ad2antlr	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to x \in [k, +∞)$
40		funfvima	$⊢ (Fun ({F ↾}_{A}) \land x \in dom ({F ↾}_{A})) \to (x \in [k, +∞) \to ({F ↾}_{A}) (x) \in ({F ↾}_{A}) [[k, +∞)])$
41	37 39 40	sylc	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to ({F ↾}_{A}) (x) \in ({F ↾}_{A}) [[k, +∞)]$
42	29 41	eqeltrd	$⊢ (((φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \land x \in (dom F \cap [k, +∞))) \land F (x) = y) \to y \in ({F ↾}_{A}) [[k, +∞)]$
43	42	rexlimdva2	$⊢ (φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \to (\exists x \in (dom F \cap [k, +∞)) F (x) = y \to y \in ({F ↾}_{A}) [[k, +∞)])$
44	10 43	mpd	$⊢ (φ \land y \in (F [[k, +∞)] \cap ℝ^{*})) \to y \in ({F ↾}_{A}) [[k, +∞)]$
45	44	ralrimiva	$⊢ φ \to \forall y \in (F [[k, +∞)] \cap ℝ^{*}) y \in ({F ↾}_{A}) [[k, +∞)]$
46		dfss3	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ({F ↾}_{A}) [[k, +∞)] \leftrightarrow \forall y \in (F [[k, +∞)] \cap ℝ^{}) y \in ({F ↾}_{A}) [[k, +∞)]$
47	45 46	sylibr	$⊢ φ \to F [[k, +∞)] \cap ℝ^{*} \subseteq ({F ↾}_{A}) [[k, +∞)]$
48		inss2	$⊢ F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
49	48	a1i	$⊢ φ \to F [[k, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
50	47 49	ssind	$⊢ φ \to F [[k, +∞)] \cap ℝ^{} \subseteq ({F ↾}_{A}) [[k, +∞)] \cap ℝ^{}$
51	6 50	eqssd	$⊢ φ \to ({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} = F [[k, +∞)] \cap ℝ^{}$
52	51	infeq1d	$⊢ φ \to inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <) = inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)$
53	52	mpteq2dv	$⊢ φ \to (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
54	53	rneqd	$⊢ φ \to ran (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
55	54	supeq1d	$⊢ φ \to sup (ran (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
56	1	resexd	$⊢ φ \to {F ↾}_{A} \in V$
57		eqid	$⊢ (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
58	57	liminfval	$⊢ {F ↾}_{A} \in V \to lim inf ({F ↾}_{A}) = sup (ran (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
59	56 58	syl	$⊢ φ \to lim inf ({F ↾}_{A}) = sup (ran (k \in ℝ ⟼ inf (({F ↾}_{A}) [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
60		eqid	$⊢ (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) = (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
61	60	liminfval	$⊢ F \in V \to lim inf (F) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
62	1 61	syl	$⊢ φ \to lim inf (F) = sup (ran (k \in ℝ ⟼ inf (F [[k, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
63	55 59 62	3eqtr4d	$⊢ φ \to lim inf ({F ↾}_{A}) = lim inf (F)$

Metamath Proof Explorer

Theorem liminfresxr

Proof