liminfvalxr - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > liminfvalxr		Structured version Visualization version GIF version

Theorem liminfvalxr 44798

Description: Alternate definition of lim inf when 𝐹 is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

**Hypotheses**
Ref	Expression
liminfvalxr.1	⊢ Ⅎ𝑥𝐹
liminfvalxr.2	⊢ (𝜑 → 𝐴 ∈ 𝑉)
liminfvalxr.3	⊢ (𝜑 → 𝐹:𝐴⟶ℝ^*)

**Assertion**
Ref	Expression
liminfvalxr	⊢ (𝜑 → (lim inf‘𝐹) = -_𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑥))))

Distinct variable group: 𝑥,𝐴 Allowed substitution hints: 𝜑(𝑥) 𝐹(𝑥) 𝑉(𝑥)

Proof of Theorem liminfvalxr Dummy variables 𝑘 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nftru 1805	. . . . . . 7 ⊢ Ⅎ𝑘⊤
2		inss2 4229	. . . . . . . . 9 ⊢ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^) ⊆ ℝ^
3		infxrcl 13317	. . . . . . . . 9 ⊢ (((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^) ⊆ ℝ^ → inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
4	2, 3	ax-mp 5	. . . . . . . 8 ⊢ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*
5	4	a1i 11	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℝ) → inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) ∈ ℝ^*)
6	1, 5	supminfxrrnmpt 44480	. . . . . 6 ⊢ (⊤ → sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) = -_𝑒inf(ran (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ))
7	6	mptru 1547	. . . . 5 ⊢ sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) = -_𝑒inf(ran (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < )
8	7	a1i 11	. . . 4 ⊢ (𝜑 → sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) = -_𝑒inf(ran (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ))
9		tru 1544	. . . . . . . . . . 11 ⊢ ⊤
10		inss2 4229	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^) ⊆ ℝ^
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^) ⊆ ℝ^)
12	11	supminfxr2 44478	. . . . . . . . . . 11 ⊢ (⊤ → sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) = -_𝑒inf({𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)}, ℝ^, < ))
13	9, 12	ax-mp 5	. . . . . . . . . 10 ⊢ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) = -_𝑒inf({𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)}, ℝ^, < )
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) = -_𝑒inf({𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)}, ℝ^, < ))
15		elinel1 4195	. . . . . . . . . . . . . . . 16 ⊢ (-_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^*) → -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)))
16		nfmpt1 5256	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))
17		xnegex 13192	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -_𝑒(𝐹‘𝑦) ∈ V
18		eqid 2731	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) = (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))
19	17, 18	fnmpti 6693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) Fn 𝐴
20	19	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) Fn 𝐴)
21	20	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) Fn 𝐴)
22		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)))
23	16, 21, 22	fvelimad 6959	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧)
24	23	3adant2 1130	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ^* ∧ -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧)
25	15, 24	syl3an3 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ^* ∧ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^*)) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧)
26		elinel2 4196	. . . . . . . . . . . . . . . 16 ⊢ (-_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^) → -_𝑒𝑧 ∈ ℝ^)
27		elinel1 4195	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → 𝑦 ∈ 𝐴)
28	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → -_𝑒(𝐹‘𝑦) ∈ V)
29	18	fvmpt2 7009	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐴 ∧ -_𝑒(𝐹‘𝑦) ∈ V) → ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒(𝐹‘𝑦))
30	27, 28, 29	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒(𝐹‘𝑦))
31	30	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → -_𝑒(𝐹‘𝑦) = ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦))
32	31	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) ∧ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧) → -_𝑒(𝐹‘𝑦) = ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦))
33		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) ∧ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧) → ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧)
34	32, 33	eqtrd 2771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) ∧ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧) → -_𝑒(𝐹‘𝑦) = -_𝑒𝑧)
35	34	adantll 711	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧) → -_𝑒(𝐹‘𝑦) = -_𝑒𝑧)
36		eqcom 2738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (-_𝑒(𝐹‘𝑦) = -_𝑒𝑧 ↔ -_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
37	36	biimpi 215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (-_𝑒(𝐹‘𝑦) = -_𝑒𝑧 → -_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -_𝑒(𝐹‘𝑦) = -_𝑒𝑧) → -_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
39		simplr 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ^) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑧 ∈ ℝ^)
40		liminfvalxr.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ^*)
41	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝐹:𝐴⟶ℝ^*)
42	27	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑦 ∈ 𝐴)
43	41, 42	ffvelcdmd 7087	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (𝐹‘𝑦) ∈ ℝ^*)
44	43	adantlr 712	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ^) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (𝐹‘𝑦) ∈ ℝ^)
45		xneg11 13199	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) ∈ ℝ^*) → (-_𝑒𝑧 = -_𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
46	39, 44, 45	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (-_𝑒𝑧 = -_𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
47	46	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -_𝑒(𝐹‘𝑦) = -_𝑒𝑧) → (-_𝑒𝑧 = -_𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
48	38, 47	mpbid 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -_𝑒(𝐹‘𝑦) = -_𝑒𝑧) → 𝑧 = (𝐹‘𝑦))
49	40	ffund 6721	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Fun 𝐹)
50	49, 27	anim12i 612	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (Fun 𝐹 ∧ 𝑦 ∈ 𝐴))
51	50	simpld 494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → Fun 𝐹)
52	40	fdmd 6728	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → dom 𝐹 = 𝐴)
53	52	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 = dom 𝐹)
54	53	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝐴 = dom 𝐹)
55	42, 54	eleqtrd 2834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑦 ∈ dom 𝐹)
56	51, 55	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹))
57		elinel2 4196	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → 𝑦 ∈ (𝑘[,)+∞))
58	57	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑦 ∈ (𝑘[,)+∞))
59		funfvima 7234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑦 ∈ (𝑘[,)+∞) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘[,)+∞))))
60	56, 58, 59	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘[,)+∞)))
61	60	ad4ant13 748	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -_𝑒(𝐹‘𝑦) = -_𝑒𝑧) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘[,)+∞)))
62	48, 61	eqeltrd 2832	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -_𝑒(𝐹‘𝑦) = -_𝑒𝑧) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
63	35, 62	syldan 590	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ^*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
64	63	rexlimdva2 3156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ^*) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧 → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))))
65	64	3adant3 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ^* ∧ -_𝑒𝑧 ∈ ℝ^*) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧 → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))))
66	26, 65	syl3an3 1164	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ^* ∧ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^*)) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))‘𝑦) = -_𝑒𝑧 → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))))
67	25, 66	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ^* ∧ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^*)) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
68	67	rabssdv 4072	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^*)} ⊆ (𝐹 “ (𝑘[,)+∞)))
69		ssrab2 4077	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)} ⊆ ℝ^
70	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)} ⊆ ℝ^)
71	68, 70	ssind 4232	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)} ⊆ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^))
72	2	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^) ⊆ ℝ^)
73	40	ffnd 6718	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐴)
74	73	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*)) → 𝐹 Fn 𝐴)
75		elinel1 4195	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
76	75	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*)) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
77		fvelima2 44263	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧)
78	74, 76, 77	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*)) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧)
79		elinel2 4196	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^) → 𝑧 ∈ ℝ^)
80		eqcom 2738	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑦) = 𝑧 ↔ 𝑧 = (𝐹‘𝑦))
81	80	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑦) = 𝑧 → 𝑧 = (𝐹‘𝑦))
82	81	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → 𝑧 = (𝐹‘𝑦))
83	82	xnegeqd 44446	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → -_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
84		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → 𝑧 ∈ ℝ^*)
85	82, 84	eqeltrrd 2833	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → (𝐹‘𝑦) ∈ ℝ^*)
86	84, 85, 45	syl2anc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → (-_𝑒𝑧 = -_𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
87	83, 86	mpbid 231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → 𝑧 = (𝐹‘𝑦))
88	87	xnegeqd 44446	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ℝ^* ∧ (𝐹‘𝑦) = 𝑧) → -_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
89	88	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℝ^* → ((𝐹‘𝑦) = 𝑧 → -_𝑒𝑧 = -_𝑒(𝐹‘𝑦)))
90	89	reximdv 3169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ^* → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧 → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-_𝑒𝑧 = -_𝑒(𝐹‘𝑦)))
91	79, 90	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧 → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-_𝑒𝑧 = -_𝑒(𝐹‘𝑦)))
92	91	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*)) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧 → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-_𝑒𝑧 = -_𝑒(𝐹‘𝑦)))
93	78, 92	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*)) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
94		xnegex 13192	. . . . . . . . . . . . . . . 16 ⊢ -_𝑒𝑧 ∈ V
95		elmptima 44261	. . . . . . . . . . . . . . . 16 ⊢ (-_𝑒𝑧 ∈ V → (-_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ↔ ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-_𝑒𝑧 = -_𝑒(𝐹‘𝑦)))
96	94, 95	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (-_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ↔ ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-_𝑒𝑧 = -_𝑒(𝐹‘𝑦))
97	93, 96	sylibr 233	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^*)) → -_𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)))
98	72	sselda 3982	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^)) → 𝑧 ∈ ℝ^)
99	98	xnegcld 13284	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^)) → -_𝑒𝑧 ∈ ℝ^)
100	97, 99	elind 4194	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^)) → -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^))
101	72, 100	ssrabdv 4071	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^) ⊆ {𝑧 ∈ ℝ^ ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^*)})
102	71, 101	eqssd 3999	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)} = ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^))
103	102	infeq1d 9476	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)}, ℝ^, < ) = inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ))
104	103	xnegeqd 44446	. . . . . . . . 9 ⊢ (𝜑 → -_𝑒inf({𝑧 ∈ ℝ^* ∣ -_𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^)}, ℝ^, < ) = -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ))
105	14, 104	eqtr2d 2772	. . . . . . . 8 ⊢ (𝜑 → -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ) = sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ))
106	105	mpteq2dv 5250	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )) = (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )))
107	106	rneqd 5937	. . . . . 6 ⊢ (𝜑 → ran (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )) = ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )))
108	107	infeq1d 9476	. . . . 5 ⊢ (𝜑 → inf(ran (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) = inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ))
109	108	xnegeqd 44446	. . . 4 ⊢ (𝜑 → -_𝑒inf(ran (𝑘 ∈ ℝ ↦ -_𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) = -_𝑒inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ))
110	8, 109	eqtrd 2771	. . 3 ⊢ (𝜑 → sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ) = -_𝑒inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^, < ))
111		liminfvalxr.2	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
112	40, 111	fexd 7231	. . . 4 ⊢ (𝜑 → 𝐹 ∈ V)
113		eqid 2731	. . . . 5 ⊢ (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )) = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ))
114	113	liminfval 44774	. . . 4 ⊢ (𝐹 ∈ V → (lim inf‘𝐹) = sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
115	112, 114	syl 17	. . 3 ⊢ (𝜑 → (lim inf‘𝐹) = sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
116	111	mptexd 7228	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) ∈ V)
117		eqid 2731	. . . . . 6 ⊢ (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )) = (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < ))
118	117	limsupval 15423	. . . . 5 ⊢ ((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) ∈ V → (lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))) = inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
119	116, 118	syl 17	. . . 4 ⊢ (𝜑 → (lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))) = inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
120	119	xnegeqd 44446	. . 3 ⊢ (𝜑 → -_𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))) = -_𝑒inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ^), ℝ^, < )), ℝ^*, < ))
121	110, 115, 120	3eqtr4d 2781	. 2 ⊢ (𝜑 → (lim inf‘𝐹) = -_𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))))
122		liminfvalxr.1	. . . . . . . 8 ⊢ Ⅎ𝑥𝐹
123		nfcv 2902	. . . . . . . 8 ⊢ Ⅎ𝑥𝑦
124	122, 123	nffv 6901	. . . . . . 7 ⊢ Ⅎ𝑥(𝐹‘𝑦)
125	124	nfxneg 44470	. . . . . 6 ⊢ Ⅎ𝑥-_𝑒(𝐹‘𝑦)
126		nfcv 2902	. . . . . 6 ⊢ Ⅎ𝑦-_𝑒(𝐹‘𝑥)
127		fveq2 6891	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
128	127	xnegeqd 44446	. . . . . 6 ⊢ (𝑦 = 𝑥 → -_𝑒(𝐹‘𝑦) = -_𝑒(𝐹‘𝑥))
129	125, 126, 128	cbvmpt 5259	. . . . 5 ⊢ (𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦)) = (𝑥 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑥))
130	129	fveq2i 6894	. . . 4 ⊢ (lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))) = (lim sup‘(𝑥 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑥)))
131	130	xnegeqi 44449	. . 3 ⊢ -_𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))) = -_𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑥)))
132	131	a1i 11	. 2 ⊢ (𝜑 → -_𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑦))) = -_𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑥))))
133	121, 132	eqtrd 2771	1 ⊢ (𝜑 → (lim inf‘𝐹) = -_𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -_𝑒(𝐹‘𝑥))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ⊤wtru 1541 ∈ wcel 2105 Ⅎwnfc 2882 ∃wrex 3069 {crab 3431 Vcvv 3473 ∩ cin 3947 ⊆ wss 3948 ↦ cmpt 5231 dom cdm 5676 ran crn 5677 “ cima 5679 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7412 supcsup 9439 infcinf 9440 ℝcr 11113 +∞cpnf 11250 ℝ^*cxr 11252 < clt 11253 -_𝑒cxne 13094 [,)cico 13331 lim supclsp 15419 lim infclsi 44766

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191 ax-pre-sup 11192

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-po 5588 df-so 5589 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-er 8707 df-en 8944 df-dom 8945 df-sdom 8946 df-sup 9441 df-inf 9442 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-xneg 13097 df-limsup 15420 df-liminf 44767

This theorem is referenced by: liminfvalxrmpt 44801

W3C validator