limsupgle

Description: The defining property of the superior limit function. (Contributed by Mario Carneiro, 5-Sep-2014) (Revised by Mario Carneiro, 7-May-2016)

		Ref	Expression
	Hypothesis	limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
	Assertion	limsupgle	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (G (C) \leq A \leftrightarrow \forall j \in B (C \leq j \to F (j) \leq A))$

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	$⊢ G = (k \in ℝ ⟼ sup (F [[k, +∞)] \cap ℝ^{} ℝ^{} <))$
2	1	limsupgval	$⊢ C \in ℝ \to G (C) = sup (F [[C, +∞)] \cap ℝ^{} ℝ^{} <)$
3	2	3ad2ant2	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to G (C) = sup (F [[C, +∞)] \cap ℝ^{} ℝ^{} <)$
4	3	breq1d	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (G (C) \leq A \leftrightarrow sup (F [[C, +∞)] \cap ℝ^{} ℝ^{} <) \leq A)$
5		inss2	$⊢ F [[C, +∞)] \cap ℝ^{} \subseteq ℝ^{}$
6		simp3	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to A \in ℝ^{*}$
7		supxrleub	$⊢ (F [[C, +∞)] \cap ℝ^{} \subseteq ℝ^{} \land A \in ℝ^{}) \to (sup (F [[C, +∞)] \cap ℝ^{} ℝ^{} <) \leq A \leftrightarrow \forall x \in (F [[C, +∞)] \cap ℝ^{}) x \leq A)$
8	5 6 7	sylancr	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (sup (F [[C, +∞)] \cap ℝ^{} ℝ^{} <) \leq A \leftrightarrow \forall x \in (F [[C, +∞)] \cap ℝ^{*}) x \leq A)$
9		imassrn	$⊢ F [[C, +∞)] \subseteq ran F$
10		simp1r	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to F : B ⟶ ℝ^{*}$
11	10	frnd	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to ran F \subseteq ℝ^{*}$
12	9 11	sstrid	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to F [[C, +∞)] \subseteq ℝ^{*}$
13		df-ss	$⊢ F [[C, +∞)] \subseteq ℝ^{} \leftrightarrow F [[C, +∞)] \cap ℝ^{} = F [[C, +∞)]$
14	12 13	sylib	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to F [[C, +∞)] \cap ℝ^{*} = F [[C, +∞)]$
15		imadmres	$⊢ F [dom ({F ↾}_{[C, +∞)})] = F [[C, +∞)]$
16	14 15	eqtr4di	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to F [[C, +∞)] \cap ℝ^{*} = F [dom ({F ↾}_{[C, +∞)})]$
17	16	raleqdv	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (\forall x \in (F [[C, +∞)] \cap ℝ^{*}) x \leq A \leftrightarrow \forall x \in F [dom ({F ↾}_{[C, +∞)})] x \leq A)$
18	10	ffnd	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to F Fn B$
19	10	fdmd	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to dom F = B$
20	19	ineq2d	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to [C, +∞) \cap dom F = [C, +∞) \cap B$
21		dmres	$⊢ dom ({F ↾}_{[C, +∞)}) = [C, +∞) \cap dom F$
22		incom	$⊢ B \cap [C, +∞) = [C, +∞) \cap B$
23	20 21 22	3eqtr4g	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to dom ({F ↾}_{[C, +∞)}) = B \cap [C, +∞)$
24		inss1	$⊢ B \cap [C, +∞) \subseteq B$
25	23 24	eqsstrdi	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to dom ({F ↾}_{[C, +∞)}) \subseteq B$
26		breq1	$⊢ x = F (j) \to (x \leq A \leftrightarrow F (j) \leq A)$
27	26	ralima	$⊢ (F Fn B \land dom ({F ↾}_{[C, +∞)}) \subseteq B) \to (\forall x \in F [dom ({F ↾}_{[C, +∞)})] x \leq A \leftrightarrow \forall j \in dom ({F ↾}_{[C, +∞)}) F (j) \leq A)$
28	18 25 27	syl2anc	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (\forall x \in F [dom ({F ↾}_{[C, +∞)})] x \leq A \leftrightarrow \forall j \in dom ({F ↾}_{[C, +∞)}) F (j) \leq A)$
29	23	eleq2d	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (j \in dom ({F ↾}_{[C, +∞)}) \leftrightarrow j \in (B \cap [C, +∞)))$
30		elin	$⊢ j \in (B \cap [C, +∞)) \leftrightarrow (j \in B \land j \in [C, +∞))$
31	29 30	bitrdi	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (j \in dom ({F ↾}_{[C, +∞)}) \leftrightarrow (j \in B \land j \in [C, +∞)))$
32		simpl2	$⊢ (((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \land j \in B) \to C \in ℝ$
33		simp1l	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to B \subseteq ℝ$
34	33	sselda	$⊢ (((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \land j \in B) \to j \in ℝ$
35		elicopnf	$⊢ C \in ℝ \to (j \in [C, +∞) \leftrightarrow (j \in ℝ \land C \leq j))$
36	35	baibd	$⊢ (C \in ℝ \land j \in ℝ) \to (j \in [C, +∞) \leftrightarrow C \leq j)$
37	32 34 36	syl2anc	$⊢ (((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \land j \in B) \to (j \in [C, +∞) \leftrightarrow C \leq j)$
38	37	pm5.32da	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to ((j \in B \land j \in [C, +∞)) \leftrightarrow (j \in B \land C \leq j))$
39	31 38	bitrd	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (j \in dom ({F ↾}_{[C, +∞)}) \leftrightarrow (j \in B \land C \leq j))$
40	39	imbi1d	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to ((j \in dom ({F ↾}_{[C, +∞)}) \to F (j) \leq A) \leftrightarrow ((j \in B \land C \leq j) \to F (j) \leq A))$
41		impexp	$⊢ ((j \in B \land C \leq j) \to F (j) \leq A) \leftrightarrow (j \in B \to (C \leq j \to F (j) \leq A))$
42	40 41	bitrdi	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to ((j \in dom ({F ↾}_{[C, +∞)}) \to F (j) \leq A) \leftrightarrow (j \in B \to (C \leq j \to F (j) \leq A)))$
43	42	ralbidv2	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (\forall j \in dom ({F ↾}_{[C, +∞)}) F (j) \leq A \leftrightarrow \forall j \in B (C \leq j \to F (j) \leq A))$
44	17 28 43	3bitrd	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (\forall x \in (F [[C, +∞)] \cap ℝ^{*}) x \leq A \leftrightarrow \forall j \in B (C \leq j \to F (j) \leq A))$
45	4 8 44	3bitrd	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land C \in ℝ \land A \in ℝ^{}) \to (G (C) \leq A \leftrightarrow \forall j \in B (C \leq j \to F (j) \leq A))$

Metamath Proof Explorer

Theorem limsupgle

Proof