Theorem liminflelimsuplem 47058

Description: The superior limit is greater than or equal to the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022.)

Hypotheses

Ref	Expression
liminflelimsuplem.1	⊢ (𝜑 → 𝐹 ∈ 𝑉)
liminflelimsuplem.2	⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)

Assertion

Ref	Expression
liminflelimsuplem	⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))

Distinct variable groups:   𝑗,𝐹,𝑘   𝜑,𝑗

Allowed substitution hints:   𝜑(𝑘)   𝑉(𝑗, 𝑘)

Proof of Theorem liminflelimsuplem

Dummy variables 𝑖 𝑙 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		inss2 4137	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*) ⊆ ℝ*
2		infxrcl 13504	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*) ⊆ ℝ* → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
3	1, 2	ax-mp 5	. . . . . . . . . . . 12 ⊢ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
4	3	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
5		inss2 4137	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ℝ*
6		infxrcl 13504	. . . . . . . . . . . . 13 ⊢ (((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ℝ* → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
7	5, 6	ax-mp 5	. . . . . . . . . . . 12 ⊢ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
8	7	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
9		inss2 4137	. . . . . . . . . . . . 13 ⊢ ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*) ⊆ ℝ*
10	9	supxrcli 46717	. . . . . . . . . . . 12 ⊢ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
11	10	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
12		rexr 11394	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ ℝ → 𝑖 ∈ ℝ*)
13	12	ad2antrr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑖 ∈ ℝ*)
14		pnfxr 11402	. . . . . . . . . . . . . . . . 17 ⊢ +∞ ∈ ℝ*
15	14	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → +∞ ∈ ℝ*)
16		simpr 490	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑙 ∈ ℝ)
17		simpl 488	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑖 ∈ ℝ)
18	16, 17	ifcld 4532	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ)
19	18	rexrd 11398	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ*)
20	19	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ*)
21		icossxr 13603	. . . . . . . . . . . . . . . . . . 19 ⊢ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞) ⊆ ℝ*
22	21	sseli 3909	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞) → 𝑗 ∈ ℝ*)
23	22	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑗 ∈ ℝ*)
24		max1 13355	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑖 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
25	24	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑖 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
26		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞))
27	20, 15, 26	icogelbd 13568	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ≤ 𝑗)
28	13, 20, 23, 25, 27	xrletrd 13331	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑖 ≤ 𝑗)
29	13, 15, 28	icossico2d 13592	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝑗[,)+∞) ⊆ (𝑖[,)+∞))
30	29	imass2d 46546	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝐹 “ (𝑗[,)+∞)) ⊆ (𝐹 “ (𝑖[,)+∞)))
31	30	ssrind 4143	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*))
32		infxrss 13510	. . . . . . . . . . . . 13 ⊢ ((((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*) ∧ ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*) ⊆ ℝ*) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
33	31, 1, 32	sylancl 598	. . . . . . . . . . . 12 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
34	33	adantr 486	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
35	5	supxrcli 46717	. . . . . . . . . . . . 13 ⊢ sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
36	35	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
37	5	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ℝ*)
38		simpr 490	. . . . . . . . . . . . 13 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)
39	37, 38	infxrlesupxr 46719	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ))
40		rexr 11394	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑙 ∈ ℝ → 𝑙 ∈ ℝ*)
41	40	ad2antlr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑙 ∈ ℝ*)
42		max2 13357	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) → 𝑙 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
43	42	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑙 ≤ if(𝑖 ≤ 𝑙, 𝑙, 𝑖))
44	41, 20, 23, 43, 27	xrletrd 13331	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → 𝑙 ≤ 𝑗)
45	41, 15, 44	icossico2d 13592	. . . . . . . . . . . . . . . 16 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝑗[,)+∞) ⊆ (𝑙[,)+∞))
46	45	imass2d 46546	. . . . . . . . . . . . . . 15 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → (𝐹 “ (𝑗[,)+∞)) ⊆ (𝐹 “ (𝑙[,)+∞)))
47	46	ssrind 4143	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ⊆ ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*))
48	9	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*) ⊆ ℝ*)
49	47, 48	xrsupssd 13503	. . . . . . . . . . . . 13 ⊢ (((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
50	49	adantr 486	. . . . . . . . . . . 12 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → sup(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
51	8, 36, 11, 39, 50	xrletrd 13331	. . . . . . . . . . 11 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
52	4, 8, 11, 34, 51	xrletrd 13331	. . . . . . . . . 10 ⊢ ((((𝑖 ∈ ℝ ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
53	52	ad5ant2345 1398	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) ∧ 𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)) ∧ ((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
54		oveq1 7458	. . . . . . . . . . 11 ⊢ (𝑘 = if(𝑖 ≤ 𝑙, 𝑙, 𝑖) → (𝑘[,)+∞) = (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞))
55	54	rexeqdv 3324	. . . . . . . . . 10 ⊢ (𝑘 = if(𝑖 ≤ 𝑙, 𝑙, 𝑖) → (∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅ ↔ ∃𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅))
56		liminflelimsuplem.2	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)
57	56	ad2antrr 739	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → ∀𝑘 ∈ ℝ ∃𝑗 ∈ (𝑘[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)
58	18	adantll 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → if(𝑖 ≤ 𝑙, 𝑙, 𝑖) ∈ ℝ)
59	55, 57, 58	rspcdva 3581	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → ∃𝑗 ∈ (if(𝑖 ≤ 𝑙, 𝑙, 𝑖)[,)+∞)((𝐹 “ (𝑗[,)+∞)) ∩ ℝ*) ≠ ∅)
60	53, 59	r19.29a 3174	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ ℝ) ∧ 𝑙 ∈ ℝ) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
61	60	ralrimiva 3158	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ∀𝑙 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))
62		nfv 1949	. . . . . . . . 9 ⊢ Ⅎ𝑙𝜑
63		xrltso 13310	. . . . . . . . . . 11 ⊢ < Or ℝ*
64	63	supex 9493	. . . . . . . . . 10 ⊢ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V
65	64	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ℝ) → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ V)
66		breq2 5112	. . . . . . . . 9 ⊢ (𝑦 = sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ) → (inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦 ↔ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < )))
67	62, 65, 66	ralrnmpt3 46544	. . . . . . . 8 ⊢ (𝜑 → (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦 ↔ ∀𝑙 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < )))
68	67	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦 ↔ ∀𝑙 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < )))
69	61, 68	mpbird 260	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦)
70		oveq1 7458	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑖 → (𝑙[,)+∞) = (𝑖[,)+∞))
71	70	imaeq2d 6070	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑖 → (𝐹 “ (𝑙[,)+∞)) = (𝐹 “ (𝑖[,)+∞)))
72	71	ineq1d 4119	. . . . . . . . . 10 ⊢ (𝑙 = 𝑖 → ((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*) = ((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*))
73	72	supeq1d 9475	. . . . . . . . 9 ⊢ (𝑙 = 𝑖 → sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ) = sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
74	73	cbvmptv 5215	. . . . . . . 8 ⊢ (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
75	74	rneqi 5931	. . . . . . 7 ⊢ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < )) = ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
76	75	raleqi 3321	. . . . . 6 ⊢ (∀𝑦 ∈ ran (𝑙 ∈ ℝ ↦ sup(((𝐹 “ (𝑙[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦 ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦)
77	69, 76	sylib 221	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦)
78	1	supxrcli 46717	. . . . . . . . 9 ⊢ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
79	78	rgenw 3084	. . . . . . . 8 ⊢ ∀𝑖 ∈ ℝ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*
80		eqid 2763	. . . . . . . . 9 ⊢ (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
81	80	rnmptss 7155	. . . . . . . 8 ⊢ (∀𝑖 ∈ ℝ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ* → ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) ⊆ ℝ*)
82	79, 81	ax-mp 5	. . . . . . 7 ⊢ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) ⊆ ℝ*
83	82	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) ⊆ ℝ*)
84		infxrgelb 13506	. . . . . 6 ⊢ ((ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) ⊆ ℝ* ∧ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*) → (inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦))
85	83, 3, 84	sylancl 598	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → (inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ↔ ∀𝑦 ∈ ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ 𝑦))
86	77, 85	mpbird 260	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
87	86	ralrimiva 3158	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
88		nfv 1949	. . . 4 ⊢ Ⅎ𝑖𝜑
89		nfcv 2926	. . . 4 ⊢ Ⅎ𝑖ℝ
90		nfmpt1 5210	. . . . . 6 ⊢ Ⅎ𝑖(𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
91	90	nfrn 5946	. . . . 5 ⊢ Ⅎ𝑖ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
92		nfcv 2926	. . . . 5 ⊢ Ⅎ𝑖ℝ*
93		nfcv 2926	. . . . 5 ⊢ Ⅎ𝑖 <
94	91, 92, 93	nfinf 9512	. . . 4 ⊢ Ⅎ𝑖inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )
95	3	a1i 11	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ ℝ) → inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ∈ ℝ*)
96		infxrcl 13504	. . . . . 6 ⊢ (ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) ⊆ ℝ* → inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ∈ ℝ*)
97	82, 96	ax-mp 5	. . . . 5 ⊢ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ∈ ℝ*
98	97	a1i 11	. . . 4 ⊢ (𝜑 → inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ∈ ℝ*)
99	88, 89, 94, 95, 98	supxrleubrnmptf 46734	. . 3 ⊢ (𝜑 → (sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ↔ ∀𝑖 ∈ ℝ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < )))
100	87, 99	mpbird 260	. 2 ⊢ (𝜑 → sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ) ≤ inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
101		liminflelimsuplem.1	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑉)
102		eqid 2763	. . 3 ⊢ (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )) = (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < ))
103	101, 102	liminfvald 47047	. 2 ⊢ (𝜑 → (lim inf‘𝐹) = sup(ran (𝑖 ∈ ℝ ↦ inf(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
104	101, 80	limsupvald 47038	. 2 ⊢ (𝜑 → (lim sup‘𝐹) = inf(ran (𝑖 ∈ ℝ ↦ sup(((𝐹 “ (𝑖[,)+∞)) ∩ ℝ*), ℝ*, < )), ℝ*, < ))
105	100, 103, 104	3brtr4d 5143	1 ⊢ (𝜑 → (lim inf‘𝐹) ≤ (lim sup‘𝐹))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  Vcvv 3454   ⊆ wss 3900   ∩ cin 4092  ∅c0 4281  ifcif 4485   class class class wbr 5108   ↦ cmpt 5192  ran crn 5659   “ cima 5661  ‘cfv 6566  (class class class)co 7451  supcsup 9469  infcinf 9470  ℝcr 11238  +∞cpnf 11379  ℝ^*cxr 11381   < clt 11382   ≤ cle 11383  [,)cico 13518  lim supclsp 15681  lim infclsi 47034

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-po 5566  df-so 5567  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-sup 9471  df-inf 9472  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-ico 13522  df-limsup 15682  df-liminf 47035

This theorem is used by:  liminflelimsup  47059