Theorem liminfvalxr 45788

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 1804	. . . . . . 7 ⊢ Ⅎ𝑘⊤
2		inss2 4204	. . . . . . . . 9 ⊢ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*
3		infxrcl 13301	. . . . . . . . 9 ⊢ (((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ* → inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
4	2, 3	ax-mp 5	. . . . . . . 8 ⊢ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
5	4	a1i 11	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℝ) → inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
6	1, 5	supminfxrrnmpt 45474	. . . . . 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 4204	. . . . . . . . . . . . 13 ⊢ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*
11	10	a1i 11	. . . . . . . . . . . 12 ⊢ (⊤ → (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*)
12	11	supminfxr2 45472	. . . . . . . . . . 11 ⊢ (⊤ → sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = -𝑒inf({𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)}, ℝ*, < ))
13	9, 12	ax-mp 5	. . . . . . . . . 10 ⊢ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = -𝑒inf({𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)}, ℝ*, < )
14	13	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = -𝑒inf({𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)}, ℝ*, < ))
15		elinel1 4167	. . . . . . . . . . . . . . . 16 ⊢ (-𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*) → -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)))
16		nfmpt1 5209	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎ𝑦(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))
17		xnegex 13175	. . . . . . . . . . . . . . . . . . . . 21 ⊢ -𝑒(𝐹‘𝑦) ∈ V
18		eqid 2730	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) = (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))
19	17, 18	fnmpti 6664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) Fn 𝐴
20	19	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) Fn 𝐴)
21	20	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) Fn 𝐴)
22		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)))
23	16, 21, 22	fvelimad 6931	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧)
24	23	3adant2 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞))) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧)
25	15, 24	syl3an3 1165	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧)
26		elinel2 4168	. . . . . . . . . . . . . . . 16 ⊢ (-𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*) → -𝑒𝑧 ∈ ℝ*)
27		elinel1 4167	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → 𝑦 ∈ 𝐴)
28	17	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → -𝑒(𝐹‘𝑦) ∈ V)
29	18	fvmpt2 6982	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑦 ∈ 𝐴 ∧ -𝑒(𝐹‘𝑦) ∈ V) → ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒(𝐹‘𝑦))
30	27, 28, 29	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒(𝐹‘𝑦))
31	30	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → -𝑒(𝐹‘𝑦) = ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦))
32	31	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) ∧ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧) → -𝑒(𝐹‘𝑦) = ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦))
33		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) ∧ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧) → ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧)
34	32, 33	eqtrd 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) ∧ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧) → -𝑒(𝐹‘𝑦) = -𝑒𝑧)
35	34	adantll 714	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧) → -𝑒(𝐹‘𝑦) = -𝑒𝑧)
36		eqcom 2737	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (-𝑒(𝐹‘𝑦) = -𝑒𝑧 ↔ -𝑒𝑧 = -𝑒(𝐹‘𝑦))
37	36	biimpi 216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (-𝑒(𝐹‘𝑦) = -𝑒𝑧 → -𝑒𝑧 = -𝑒(𝐹‘𝑦))
38	37	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -𝑒(𝐹‘𝑦) = -𝑒𝑧) → -𝑒𝑧 = -𝑒(𝐹‘𝑦))
39		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑧 ∈ ℝ*)
40		liminfvalxr.3	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → 𝐹:𝐴⟶ℝ*)
41	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝐹:𝐴⟶ℝ*)
42	27	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑦 ∈ 𝐴)
43	41, 42	ffvelcdmd 7060	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (𝐹‘𝑦) ∈ ℝ*)
44	43	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (𝐹‘𝑦) ∈ ℝ*)
45		xneg11 13182	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) ∈ ℝ*) → (-𝑒𝑧 = -𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
46	39, 44, 45	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (-𝑒𝑧 = -𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
47	46	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -𝑒(𝐹‘𝑦) = -𝑒𝑧) → (-𝑒𝑧 = -𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
48	38, 47	mpbid 232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -𝑒(𝐹‘𝑦) = -𝑒𝑧) → 𝑧 = (𝐹‘𝑦))
49	40	ffund 6695	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → Fun 𝐹)
50	49, 27	anim12i 613	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (Fun 𝐹 ∧ 𝑦 ∈ 𝐴))
51	50	simpld 494	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → Fun 𝐹)
52	40	fdmd 6701	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝜑 → dom 𝐹 = 𝐴)
53	52	eqcomd 2736	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → 𝐴 = dom 𝐹)
54	53	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝐴 = dom 𝐹)
55	42, 54	eleqtrd 2831	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑦 ∈ dom 𝐹)
56	51, 55	jca 511	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹))
57		elinel2 4168	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞)) → 𝑦 ∈ (𝑘[,)+∞))
58	57	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → 𝑦 ∈ (𝑘[,)+∞))
59		funfvima 7207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((Fun 𝐹 ∧ 𝑦 ∈ dom 𝐹) → (𝑦 ∈ (𝑘[,)+∞) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘[,)+∞))))
60	56, 58, 59	sylc 65	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘[,)+∞)))
61	60	ad4ant13 751	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -𝑒(𝐹‘𝑦) = -𝑒𝑧) → (𝐹‘𝑦) ∈ (𝐹 “ (𝑘[,)+∞)))
62	48, 61	eqeltrd 2829	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ -𝑒(𝐹‘𝑦) = -𝑒𝑧) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
63	35, 62	syldan 591	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝜑 ∧ 𝑧 ∈ ℝ*) ∧ 𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))) ∧ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
64	63	rexlimdva2 3137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ*) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧 → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))))
65	64	3adant3 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒𝑧 ∈ ℝ*) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧 → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))))
66	26, 65	syl3an3 1165	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))‘𝑦) = -𝑒𝑧 → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))))
67	25, 66	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ℝ* ∧ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
68	67	rabssdv 4041	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)} ⊆ (𝐹 “ (𝑘[,)+∞)))
69		ssrab2 4046	. . . . . . . . . . . . . 14 ⊢ {𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)} ⊆ ℝ*
70	69	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)} ⊆ ℝ*)
71	68, 70	ssind 4207	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)} ⊆ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
72	2	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ ℝ*)
73	40	ffnd 6692	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐹 Fn 𝐴)
74	73	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → 𝐹 Fn 𝐴)
75		elinel1 4167	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
76	75	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → 𝑧 ∈ (𝐹 “ (𝑘[,)+∞)))
77		fvelima2 6916	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑧 ∈ (𝐹 “ (𝑘[,)+∞))) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧)
78	74, 76, 77	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧)
79		elinel2 4168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) → 𝑧 ∈ ℝ*)
80		eqcom 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝐹‘𝑦) = 𝑧 ↔ 𝑧 = (𝐹‘𝑦))
81	80	biimpi 216	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐹‘𝑦) = 𝑧 → 𝑧 = (𝐹‘𝑦))
82	81	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → 𝑧 = (𝐹‘𝑦))
83	82	xnegeqd 45440	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → -𝑒𝑧 = -𝑒(𝐹‘𝑦))
84		simpl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → 𝑧 ∈ ℝ*)
85	82, 84	eqeltrrd 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → (𝐹‘𝑦) ∈ ℝ*)
86	84, 85, 45	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → (-𝑒𝑧 = -𝑒(𝐹‘𝑦) ↔ 𝑧 = (𝐹‘𝑦)))
87	83, 86	mpbid 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → 𝑧 = (𝐹‘𝑦))
88	87	xnegeqd 45440	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ ℝ* ∧ (𝐹‘𝑦) = 𝑧) → -𝑒𝑧 = -𝑒(𝐹‘𝑦))
89	88	ex 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 ∈ ℝ* → ((𝐹‘𝑦) = 𝑧 → -𝑒𝑧 = -𝑒(𝐹‘𝑦)))
90	89	reximdv 3149	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑧 ∈ ℝ* → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧 → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-𝑒𝑧 = -𝑒(𝐹‘𝑦)))
91	79, 90	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧 → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-𝑒𝑧 = -𝑒(𝐹‘𝑦)))
92	91	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → (∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))(𝐹‘𝑦) = 𝑧 → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-𝑒𝑧 = -𝑒(𝐹‘𝑦)))
93	78, 92	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-𝑒𝑧 = -𝑒(𝐹‘𝑦))
94		xnegex 13175	. . . . . . . . . . . . . . . 16 ⊢ -𝑒𝑧 ∈ V
95		elmptima 45259	. . . . . . . . . . . . . . . 16 ⊢ (-𝑒𝑧 ∈ V → (-𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ↔ ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-𝑒𝑧 = -𝑒(𝐹‘𝑦)))
96	94, 95	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (-𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ↔ ∃𝑦 ∈ (𝐴 ∩ (𝑘[,)+∞))-𝑒𝑧 = -𝑒(𝐹‘𝑦))
97	93, 96	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → -𝑒𝑧 ∈ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)))
98	72	sselda 3949	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → 𝑧 ∈ ℝ*)
99	98	xnegcld 13267	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → -𝑒𝑧 ∈ ℝ*)
100	97, 99	elind 4166	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*)) → -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*))
101	72, 100	ssrabdv 4040	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*) ⊆ {𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)})
102	71, 101	eqssd 3967	. . . . . . . . . . 11 ⊢ (𝜑 → {𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)} = ((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*))
103	102	infeq1d 9436	. . . . . . . . . 10 ⊢ (𝜑 → inf({𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)}, ℝ*, < ) = inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
104	103	xnegeqd 45440	. . . . . . . . 9 ⊢ (𝜑 → -𝑒inf({𝑧 ∈ ℝ* ∣ -𝑒𝑧 ∈ (((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*)}, ℝ*, < ) = -𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
105	14, 104	eqtr2d 2766	. . . . . . . 8 ⊢ (𝜑 → -𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ) = sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
106	105	mpteq2dv 5204	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ℝ ↦ -𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )))
107	106	rneqd 5905	. . . . . 6 ⊢ (𝜑 → ran (𝑘 ∈ ℝ ↦ -𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )))
108	107	infeq1d 9436	. . . . 5 ⊢ (𝜑 → inf(ran (𝑘 ∈ ℝ ↦ -𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) = inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
109	108	xnegeqd 45440	. . . 4 ⊢ (𝜑 → -𝑒inf(ran (𝑘 ∈ ℝ ↦ -𝑒inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) = -𝑒inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
110	8, 109	eqtrd 2765	. . 3 ⊢ (𝜑 → sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) = -𝑒inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
111		liminfvalxr.2	. . . . 5 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
112	40, 111	fexd 7204	. . . 4 ⊢ (𝜑 → 𝐹 ∈ V)
113		eqid 2730	. . . . 5 ⊢ (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
114	113	liminfval 45764	. . . 4 ⊢ (𝐹 ∈ V → (lim inf‘𝐹) = sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
115	112, 114	syl 17	. . 3 ⊢ (𝜑 → (lim inf‘𝐹) = sup(ran (𝑘 ∈ ℝ ↦ inf(((𝐹 “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
116	111	mptexd 7201	. . . . 5 ⊢ (𝜑 → (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) ∈ V)
117		eqid 2730	. . . . . 6 ⊢ (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < ))
118	117	limsupval 15447	. . . . 5 ⊢ ((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) ∈ V → (lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))) = inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
119	116, 118	syl 17	. . . 4 ⊢ (𝜑 → (lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))) = inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
120	119	xnegeqd 45440	. . 3 ⊢ (𝜑 → -𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))) = -𝑒inf(ran (𝑘 ∈ ℝ ↦ sup((((𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) “ (𝑘[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
121	110, 115, 120	3eqtr4d 2775	. 2 ⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))))
122		liminfvalxr.1	. . . . . . . 8 ⊢ Ⅎ𝑥𝐹
123		nfcv 2892	. . . . . . . 8 ⊢ Ⅎ𝑥𝑦
124	122, 123	nffv 6871	. . . . . . 7 ⊢ Ⅎ𝑥(𝐹‘𝑦)
125	124	nfxneg 45464	. . . . . 6 ⊢ Ⅎ𝑥-𝑒(𝐹‘𝑦)
126		nfcv 2892	. . . . . 6 ⊢ Ⅎ𝑦-𝑒(𝐹‘𝑥)
127		fveq2 6861	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝐹‘𝑦) = (𝐹‘𝑥))
128	127	xnegeqd 45440	. . . . . 6 ⊢ (𝑦 = 𝑥 → -𝑒(𝐹‘𝑦) = -𝑒(𝐹‘𝑥))
129	125, 126, 128	cbvmpt 5212	. . . . 5 ⊢ (𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦)) = (𝑥 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑥))
130	129	fveq2i 6864	. . . 4 ⊢ (lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))) = (lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑥)))
131	130	xnegeqi 45443	. . 3 ⊢ -𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑥)))
132	131	a1i 11	. 2 ⊢ (𝜑 → -𝑒(lim sup‘(𝑦 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑦))) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑥))))
133	121, 132	eqtrd 2765	1 ⊢ (𝜑 → (lim inf‘𝐹) = -𝑒(lim sup‘(𝑥 ∈ 𝐴 ↦ -𝑒(𝐹‘𝑥))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109  Ⅎwnfc 2877  ∃wrex 3054  {crab 3408  Vcvv 3450   ∩ cin 3916   ⊆ wss 3917   ↦ cmpt 5191  dom cdm 5641  ran crn 5642   “ cima 5644  Fun wfun 6508   Fn wfn 6509  ⟶wf 6510  ‘cfv 6514  (class class class)co 7390  supcsup 9398  infcinf 9399  ℝcr 11074  +∞cpnf 11212  ℝ^*cxr 11214   < clt 11215  -_𝑒cxne 13076  [,)cico 13315  lim supclsp 15443  lim infclsi 45756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-rep 5237  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rmo 3356  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-po 5549  df-so 5550  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-isom 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-sup 9400  df-inf 9401  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221  df-sub 11414  df-neg 11415  df-xneg 13079  df-limsup 15444  df-liminf 45757

This theorem is referenced by:  liminfvalxrmpt  45791