limsupval2

Description: The superior limit, relativized to an unbounded set. (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
	limsupval2.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	limsupval2.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	limsupval2.3	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) = +∞ )
Assertion	limsupval2	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		limsupval.1	⊢ 𝐺 = ( 𝑘 ∈ ℝ ↦ sup ( ( ( 𝐹 “ ( 𝑘 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
2		limsupval2.1	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		limsupval2.2	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
4		limsupval2.3	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) = +∞ )
5	1	limsupval	⊢ ( 𝐹 ∈ 𝑉 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ^* , < ) )
6	2 5	syl	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ran 𝐺 , ℝ^* , < ) )
7		imassrn	⊢ ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺
8	1	limsupgf	⊢ 𝐺 : ℝ ⟶ ℝ^*
9		frn	⊢ ( 𝐺 : ℝ ⟶ ℝ^* → ran 𝐺 ⊆ ℝ^* )
10	8 9	ax-mp	⊢ ran 𝐺 ⊆ ℝ^*
11		infxrlb	⊢ ( ( ran 𝐺 ⊆ ℝ^* ∧ 𝑥 ∈ ran 𝐺 ) → inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 )
12	11	ralrimiva	⊢ ( ran 𝐺 ⊆ ℝ^* → ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 )
13	10 12	mp1i	⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 )
14		ssralv	⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ran 𝐺 → ( ∀ 𝑥 ∈ ran 𝐺 inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 → ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 ) )
15	7 13 14	mpsyl	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 )
16	7 10	sstri	⊢ ( 𝐺 “ 𝐴 ) ⊆ ℝ^*
17		infxrcl	⊢ ( ran 𝐺 ⊆ ℝ^* → inf ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^* )
18	10 17	ax-mp	⊢ inf ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^*
19		infxrgelb	⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ^* ∧ inf ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^* ) → ( inf ( ran 𝐺 , ℝ^* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 ) )
20	16 18 19	mp2an	⊢ ( inf ( ran 𝐺 , ℝ^* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ∀ 𝑥 ∈ ( 𝐺 “ 𝐴 ) inf ( ran 𝐺 , ℝ^* , < ) ≤ 𝑥 )
21	15 20	sylibr	⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ^* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
22		ressxr	⊢ ℝ ⊆ ℝ^*
23	3 22	sstrdi	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
24		supxrunb1	⊢ ( 𝐴 ⊆ ℝ^* → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ^* , < ) = +∞ ) )
25	23 24	syl	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 ↔ sup ( 𝐴 , ℝ^* , < ) = +∞ ) )
26	4 25	mpbird	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 )
27		infxrcl	⊢ ( ( 𝐺 “ 𝐴 ) ⊆ ℝ^* → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* )
28	16 27	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* )
29	3	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
30	29	ad2ant2r	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
31	8	ffvelcdmi	⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) ∈ ℝ^* )
32	30 31	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ^* )
33	8	ffvelcdmi	⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) ∈ ℝ^* )
34	33	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) ∈ ℝ^* )
35		ffn	⊢ ( 𝐺 : ℝ ⟶ ℝ^* → 𝐺 Fn ℝ )
36	8 35	mp1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐺 Fn ℝ )
37	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝐴 ⊆ ℝ )
38		simprl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
39		fnfvima	⊢ ( ( 𝐺 Fn ℝ ∧ 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
40	36 37 38 39	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) )
41		infxrlb	⊢ ( ( ( 𝐺 “ 𝐴 ) ⊆ ℝ^* ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( 𝐺 “ 𝐴 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑥 ) )
42	16 40 41	sylancr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑥 ) )
43		simplr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ∈ ℝ )
44		simprr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → 𝑛 ≤ 𝑥 )
45		limsupgord	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑛 ≤ 𝑥 ) → sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
46	43 30 44 45	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) ≤ sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
47	1	limsupgval	⊢ ( 𝑥 ∈ ℝ → ( 𝐺 ‘ 𝑥 ) = sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
48	30 47	syl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) = sup ( ( ( 𝐹 “ ( 𝑥 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
49	1	limsupgval	⊢ ( 𝑛 ∈ ℝ → ( 𝐺 ‘ 𝑛 ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
50	49	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑛 ) = sup ( ( ( 𝐹 “ ( 𝑛 [,) +∞ ) ) ∩ ℝ^* ) , ℝ^* , < ) )
51	46 48 50	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → ( 𝐺 ‘ 𝑥 ) ≤ ( 𝐺 ‘ 𝑛 ) )
52	28 32 34 42 51	xrletrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑛 ≤ 𝑥 ) ) → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) )
53	52	rexlimdvaa	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℝ ) → ( ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
54	53	ralimdva	⊢ ( 𝜑 → ( ∀ 𝑛 ∈ ℝ ∃ 𝑥 ∈ 𝐴 𝑛 ≤ 𝑥 → ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
55	26 54	mpd	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) )
56	8 35	ax-mp	⊢ 𝐺 Fn ℝ
57		breq2	⊢ ( 𝑥 = ( 𝐺 ‘ 𝑛 ) → ( inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ 𝑥 ↔ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
58	57	ralrn	⊢ ( 𝐺 Fn ℝ → ( ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) ) )
59	56 58	ax-mp	⊢ ( ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ 𝑥 ↔ ∀ 𝑛 ∈ ℝ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ ( 𝐺 ‘ 𝑛 ) )
60	55 59	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ 𝑥 )
61	16 27	ax-mp	⊢ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^*
62		infxrgelb	⊢ ( ( ran 𝐺 ⊆ ℝ^* ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* ) → ( inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ inf ( ran 𝐺 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ 𝑥 ) )
63	10 61 62	mp2an	⊢ ( inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ inf ( ran 𝐺 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ ran 𝐺 inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ 𝑥 )
64	60 63	sylibr	⊢ ( 𝜑 → inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ inf ( ran 𝐺 , ℝ^* , < ) )
65		xrletri3	⊢ ( ( inf ( ran 𝐺 , ℝ^* , < ) ∈ ℝ^* ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∈ ℝ^* ) → ( inf ( ran 𝐺 , ℝ^* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ( inf ( ran 𝐺 , ℝ^* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ inf ( ran 𝐺 , ℝ^* , < ) ) ) )
66	18 61 65	mp2an	⊢ ( inf ( ran 𝐺 , ℝ^* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ↔ ( inf ( ran 𝐺 , ℝ^* , < ) ≤ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ∧ inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) ≤ inf ( ran 𝐺 , ℝ^* , < ) ) )
67	21 64 66	sylanbrc	⊢ ( 𝜑 → inf ( ran 𝐺 , ℝ^* , < ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )
68	6 67	eqtrd	⊢ ( 𝜑 → ( lim sup ‘ 𝐹 ) = inf ( ( 𝐺 “ 𝐴 ) , ℝ^* , < ) )

Metamath Proof Explorer

Theorem limsupval2

Proof