liminflelimsuplem

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

	Ref	Expression
Hypotheses	liminflelimsuplem.1	$⊢ φ \to F \in V$
	liminflelimsuplem.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
Assertion	liminflelimsuplem	$⊢ φ \to lim inf (F) \leq lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		liminflelimsuplem.1	$⊢ φ \to F \in V$
2		liminflelimsuplem.2	$⊢ φ \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
3		simpr	$⊢ (i \in ℝ \land l \in ℝ) \to l \in ℝ$
4		simpl	$⊢ (i \in ℝ \land l \in ℝ) \to i \in ℝ$
5	3 4	ifcld	$⊢ (i \in ℝ \land l \in ℝ) \to if (i \leq l, l, i) \in ℝ$
6	5	adantll	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to if (i \leq l, l, i) \in ℝ$
7	2	ad2antrr	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
8		oveq1	$⊢ k = if (i \leq l, l, i) \to [k, +∞) = [if (i \leq l, l, i), +∞)$
9	8	rexeqdv	$⊢ k = if (i \leq l, l, i) \to (\exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \leftrightarrow \exists j \in [if (i \leq l, l, i), +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset)$
10	9	rspcva	$⊢ (if (i \leq l, l, i) \in ℝ \land \forall k \in ℝ \exists j \in [k, +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to \exists j \in [if (i \leq l, l, i), +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset$
11	6 7 10	syl2anc	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to \exists j \in [if (i \leq l, l, i), +∞) F [[j, +∞)] \cap ℝ^{*} \neq \emptyset$
12		inss2	$⊢ F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
13		infxrcl	$⊢ F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
14	12 13	ax-mp	$⊢ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
15	14	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
16		inss2	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
17		infxrcl	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
18	16 17	ax-mp	$⊢ inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
19	18	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
20		inss2	$⊢ F [[l, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
21		supxrcl	$⊢ F [[l, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
22	20 21	ax-mp	$⊢ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
23	22	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
24		rexr	$⊢ i \in ℝ \to i \in ℝ^{*}$
25	24	ad2antrr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to i \in ℝ^{*}$
26		pnfxr	$⊢ +∞ \in ℝ^{*}$
27	26	a1i	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to +∞ \in ℝ^{*}$
28	5	rexrd	$⊢ (i \in ℝ \land l \in ℝ) \to if (i \leq l, l, i) \in ℝ^{*}$
29	28	adantr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to if (i \leq l, l, i) \in ℝ^{*}$
30		icossxr	$⊢ [if (i \leq l, l, i), +∞) \subseteq ℝ^{*}$
31		id	$⊢ j \in [if (i \leq l, l, i), +∞) \to j \in [if (i \leq l, l, i), +∞)$
32	30 31	sselid	$⊢ j \in [if (i \leq l, l, i), +∞) \to j \in ℝ^{*}$
33	32	adantl	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to j \in ℝ^{*}$
34		max1	$⊢ (i \in ℝ \land l \in ℝ) \to i \leq if (i \leq l, l, i)$
35	34	adantr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to i \leq if (i \leq l, l, i)$
36		simpr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to j \in [if (i \leq l, l, i), +∞)$
37	29 27 36	icogelbd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to if (i \leq l, l, i) \leq j$
38	25 29 33 35 37	xrletrd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to i \leq j$
39	25 27 38	icossico2	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to [j, +∞) \subseteq [i, +∞)$
40	39	imass2d	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \subseteq F [[i, +∞)]$
41	40	ssrind	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \cap ℝ^{} \subseteq F [[i, +∞)] \cap ℝ^{}$
42	12	a1i	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
43		infxrss	$⊢ (F [[j, +∞)] \cap ℝ^{} \subseteq F [[i, +∞)] \cap ℝ^{} \land F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{}) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)$
44	41 42 43	syl2anc	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <)$
45	44	adantr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (F [[j, +∞)] \cap ℝ^{} ℝ^{*} <)$
46		supxrcl	$⊢ F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
47	16 46	ax-mp	$⊢ sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
48	47	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}$
49	16	a1i	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to F [[j, +∞)] \cap ℝ^{} \subseteq ℝ^{*}$
50		simpr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to F [[j, +∞)] \cap ℝ^{} \neq \emptyset$
51	49 50	infxrlesupxr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[j, +∞)] \cap ℝ^{} ℝ^{*} <)$
52		rexr	$⊢ l \in ℝ \to l \in ℝ^{*}$
53	52	ad2antlr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to l \in ℝ^{*}$
54		max2	$⊢ (i \in ℝ \land l \in ℝ) \to l \leq if (i \leq l, l, i)$
55	54	adantr	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to l \leq if (i \leq l, l, i)$
56	53 29 33 55 37	xrletrd	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to l \leq j$
57	53 27 56	icossico2	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to [j, +∞) \subseteq [l, +∞)$
58	57	imass2d	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \subseteq F [[l, +∞)]$
59	58	ssrind	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[j, +∞)] \cap ℝ^{} \subseteq F [[l, +∞)] \cap ℝ^{}$
60	20	a1i	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to F [[l, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
61		supxrss	$⊢ (F [[j, +∞)] \cap ℝ^{} \subseteq F [[l, +∞)] \cap ℝ^{} \land F [[l, +∞)] \cap ℝ^{} \subseteq ℝ^{}) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
62	59 60 61	syl2anc	$⊢ ((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
63	62	adantr	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to sup (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
64	19 48 23 51 63	xrletrd	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[j, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
65	15 19 23 45 64	xrletrd	$⊢ (((i \in ℝ \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
66	65	ad5ant2345	$⊢ ((((φ \land i \in ℝ) \land l \in ℝ) \land j \in [if (i \leq l, l, i), +∞)) \land F [[j, +∞)] \cap ℝ^{} \neq \emptyset) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <)$
67	66	rexlimdva2	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to (\exists j \in [if (i \leq l, l, i), +∞) F [[j, +∞)] \cap ℝ^{} \neq \emptyset \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{*} <))$
68	11 67	mpd	$⊢ ((φ \land i \in ℝ) \land l \in ℝ) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
69	68	ralrimiva	$⊢ (φ \land i \in ℝ) \to \forall l \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)$
70		nfv	$⊢ Ⅎ l φ$
71		xrltso	$⊢ < Or ℝ^{*}$
72	71	supex	$⊢ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
73	72	a1i	$⊢ (φ \land l \in ℝ) \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \in V$
74		breq2	$⊢ y = sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) \to (inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <))$
75	70 73 74	ralrnmpt3	$⊢ φ \to (\forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall l \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <))$
76	75	adantr	$⊢ (φ \land i \in ℝ) \to (\forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall l \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <))$
77	69 76	mpbird	$⊢ (φ \land i \in ℝ) \to \forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y$
78		oveq1	$⊢ l = i \to [l, +∞) = [i, +∞)$
79	78	imaeq2d	$⊢ l = i \to F [[l, +∞)] = F [[i, +∞)]$
80	79	ineq1d	$⊢ l = i \to F [[l, +∞)] \cap ℝ^{} = F [[i, +∞)] \cap ℝ^{}$
81	80	supeq1d	$⊢ l = i \to sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <) = sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)$
82	81	cbvmptv	$⊢ (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
83	82	rneqi	$⊢ ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) = ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
84	83	raleqi	$⊢ \forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y$
85	84	a1i	$⊢ (φ \land i \in ℝ) \to (\forall y \in ran (l \in ℝ ⟼ sup (F [[l, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y)$
86	77 85	mpbid	$⊢ (φ \land i \in ℝ) \to \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq y$
87		supxrcl	$⊢ F [[i, +∞)] \cap ℝ^{} \subseteq ℝ^{} \to sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
88	12 87	ax-mp	$⊢ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
89	88	rgenw	$⊢ \forall i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
90		eqid	$⊢ (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
91	90	rnmptss	$⊢ \forall i \in ℝ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{} \to ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{}$
92	89 91	ax-mp	$⊢ ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{*}$
93	92	a1i	$⊢ (φ \land i \in ℝ) \to ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{*}$
94	14	a1i	$⊢ (φ \land i \in ℝ) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{*}$
95		infxrgelb	$⊢ (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{} \land inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \in ℝ^{}) \to (inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{*} <) \leq y)$
96	93 94 95	syl2anc	$⊢ (φ \land i \in ℝ) \to (inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leftrightarrow \forall y \in ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) inf (F [[i, +∞)] \cap ℝ^{} ℝ^{*} <) \leq y)$
97	86 96	mpbird	$⊢ (φ \land i \in ℝ) \to inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
98	97	ralrimiva	$⊢ φ \to \forall i \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
99		nfv	$⊢ Ⅎ i φ$
100		nfcv	$⊢ \underline{Ⅎ} i ℝ$
101		nfmpt1	$⊢ \underline{Ⅎ} i (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
102	101	nfrn	$⊢ \underline{Ⅎ} i ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
103		nfcv	$⊢ \underline{Ⅎ} i ℝ^{*}$
104		nfcv	$⊢ \underline{Ⅎ} i <$
105	102 103 104	nfinf	$⊢ \underline{Ⅎ} i inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
106		infxrcl	$⊢ ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) \subseteq ℝ^{} \to inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{*}$
107	92 106	ax-mp	$⊢ inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{}$
108	107	a1i	$⊢ φ \to inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \in ℝ^{}$
109	99 100 105 94 108	supxrleubrnmptf	$⊢ φ \to (sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leftrightarrow \forall i \in ℝ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <))$
110	98 109	mpbird	$⊢ φ \to sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <)$
111		eqid	$⊢ (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) = (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <))$
112	1 111	liminfvald	$⊢ φ \to lim inf (F) = sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
113	1 90	limsupvald	$⊢ φ \to lim sup (F) = inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{*} <)$
114	112 113	breq12d	$⊢ φ \to (lim inf (F) \leq lim sup (F) \leftrightarrow sup (ran (i \in ℝ ⟼ inf (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <) \leq inf (ran (i \in ℝ ⟼ sup (F [[i, +∞)] \cap ℝ^{} ℝ^{} <)) ℝ^{} <))$
115	110 114	mpbird	$⊢ φ \to lim inf (F) \leq lim sup (F)$

Metamath Proof Explorer

Theorem liminflelimsuplem

Proof