Theorem pnfneige0

Description: A neighborhood of +oo contains an unbounded interval based at a real number. See pnfnei . (Contributed by Thierry Arnoux, 31-Jul-2017)

	Ref	Expression
Hypothesis	pnfneige0.j	|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
Assertion	pnfneige0	|- ( ( A e. J /\ +oo e. A ) -> E. x e. RR ( x (,] +oo ) C_ A )

Proof

Step	Hyp	Ref	Expression
1		pnfneige0.j	|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
2		0red	|- ( ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) /\ y < 0 ) -> 0 e. RR )
3		simpllr	|- ( ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) /\ -. y < 0 ) -> y e. RR )
4	2 3	ifclda	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> if ( y < 0 , 0 , y ) e. RR )
5		ovif	|- ( if ( y < 0 , 0 , y ) (,] +oo ) = if ( y < 0 , ( 0 (,] +oo ) , ( y (,] +oo ) )
6		rexr	|- ( y e. RR -> y e. RR* )
7		0xr	|- 0 e. RR*
8	7	a1i	|- ( y e. RR -> 0 e. RR* )
9		pnfxr	|- +oo e. RR*
10	9	a1i	|- ( y e. RR -> +oo e. RR* )
11		iocinif	|- ( ( y e. RR* /\ 0 e. RR* /\ +oo e. RR* ) -> ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) = if ( y < 0 , ( 0 (,] +oo ) , ( y (,] +oo ) ) )
12	6 8 10 11	syl3anc	|- ( y e. RR -> ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) = if ( y < 0 , ( 0 (,] +oo ) , ( y (,] +oo ) ) )
13	5 12	eqtr4id	|- ( y e. RR -> ( if ( y < 0 , 0 , y ) (,] +oo ) = ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) )
14	13	ad2antlr	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> ( if ( y < 0 , 0 , y ) (,] +oo ) = ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) )
15		iocssicc	|- ( 0 (,] +oo ) C_ ( 0 [,] +oo )
16		sslin	|- ( ( 0 (,] +oo ) C_ ( 0 [,] +oo ) -> ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( ( y (,] +oo ) i^i ( 0 [,] +oo ) ) )
17	15 16	mp1i	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( ( y (,] +oo ) i^i ( 0 [,] +oo ) ) )
18		simpr	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) )
19		ssin	|- ( ( ( y (,] +oo ) C_ A /\ ( y (,] +oo ) C_ ( 0 (,] +oo ) ) <-> ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) )
20	19	biimpri	|- ( ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) -> ( ( y (,] +oo ) C_ A /\ ( y (,] +oo ) C_ ( 0 (,] +oo ) ) )
21	20	simpld	|- ( ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) -> ( y (,] +oo ) C_ A )
22		ssinss1	|- ( ( y (,] +oo ) C_ A -> ( ( y (,] +oo ) i^i ( 0 [,] +oo ) ) C_ A )
23	18 21 22	3syl	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> ( ( y (,] +oo ) i^i ( 0 [,] +oo ) ) C_ A )
24	17 23	sstrd	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> ( ( y (,] +oo ) i^i ( 0 (,] +oo ) ) C_ A )
25	14 24	eqsstrd	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> ( if ( y < 0 , 0 , y ) (,] +oo ) C_ A )
26		oveq1	|- ( x = if ( y < 0 , 0 , y ) -> ( x (,] +oo ) = ( if ( y < 0 , 0 , y ) (,] +oo ) )
27	26	sseq1d	|- ( x = if ( y < 0 , 0 , y ) -> ( ( x (,] +oo ) C_ A <-> ( if ( y < 0 , 0 , y ) (,] +oo ) C_ A ) )
28	27	rspcev	|- ( ( if ( y < 0 , 0 , y ) e. RR /\ ( if ( y < 0 , 0 , y ) (,] +oo ) C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A )
29	4 25 28	syl2anc	|- ( ( ( ( A e. J /\ +oo e. A ) /\ y e. RR ) /\ ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) ) -> E. x e. RR ( x (,] +oo ) C_ A )
30		letopon	|- ( ordTop ` <_ ) e. ( TopOn ` RR* )
31		iccssxr	|- ( 0 [,] +oo ) C_ RR*
32		resttopon	|- ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) )
33	30 31 32	mp2an	|- ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) )
34	33	topontopi	|- ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Top
35	34	a1i	|- ( A e. J -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Top )
36		ovex	|- ( 0 (,] +oo ) e. _V
37	36	a1i	|- ( A e. J -> ( 0 (,] +oo ) e. _V )
38		xrge0topn	|- ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
39	1 38	eqtri	|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) )
40	39	eleq2i	|- ( A e. J <-> A e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
41	40	biimpi	|- ( A e. J -> A e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) )
42		elrestr	|- ( ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. Top /\ ( 0 (,] +oo ) e. _V /\ A e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) -> ( A i^i ( 0 (,] +oo ) ) e. ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t ( 0 (,] +oo ) ) )
43	35 37 41 42	syl3anc	|- ( A e. J -> ( A i^i ( 0 (,] +oo ) ) e. ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t ( 0 (,] +oo ) ) )
44		letop	|- ( ordTop ` <_ ) e. Top
45		ovex	|- ( 0 [,] +oo ) e. _V
46		restabs	|- ( ( ( ordTop ` <_ ) e. Top /\ ( 0 (,] +oo ) C_ ( 0 [,] +oo ) /\ ( 0 [,] +oo ) e. _V ) -> ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t ( 0 (,] +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 (,] +oo ) ) )
47	44 15 45 46	mp3an	|- ( ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |`t ( 0 (,] +oo ) ) = ( ( ordTop ` <_ ) |`t ( 0 (,] +oo ) )
48	43 47	eleqtrdi	|- ( A e. J -> ( A i^i ( 0 (,] +oo ) ) e. ( ( ordTop ` <_ ) |`t ( 0 (,] +oo ) ) )
49	44	a1i	|- ( A e. J -> ( ordTop ` <_ ) e. Top )
50		iocpnfordt	|- ( 0 (,] +oo ) e. ( ordTop ` <_ )
51	50	a1i	|- ( A e. J -> ( 0 (,] +oo ) e. ( ordTop ` <_ ) )
52		ssidd	|- ( A e. J -> ( 0 (,] +oo ) C_ ( 0 (,] +oo ) )
53		inss2	|- ( A i^i ( 0 (,] +oo ) ) C_ ( 0 (,] +oo )
54	53	a1i	|- ( A e. J -> ( A i^i ( 0 (,] +oo ) ) C_ ( 0 (,] +oo ) )
55		restopnb	|- ( ( ( ( ordTop ` <_ ) e. Top /\ ( 0 (,] +oo ) e. _V ) /\ ( ( 0 (,] +oo ) e. ( ordTop ` <_ ) /\ ( 0 (,] +oo ) C_ ( 0 (,] +oo ) /\ ( A i^i ( 0 (,] +oo ) ) C_ ( 0 (,] +oo ) ) ) -> ( ( A i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) <-> ( A i^i ( 0 (,] +oo ) ) e. ( ( ordTop ` <_ ) |`t ( 0 (,] +oo ) ) ) )
56	49 37 51 52 54 55	syl23anc	|- ( A e. J -> ( ( A i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) <-> ( A i^i ( 0 (,] +oo ) ) e. ( ( ordTop ` <_ ) |`t ( 0 (,] +oo ) ) ) )
57	48 56	mpbird	|- ( A e. J -> ( A i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) )
58	57	adantr	|- ( ( A e. J /\ +oo e. A ) -> ( A i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) )
59		simpr	|- ( ( A e. J /\ +oo e. A ) -> +oo e. A )
60		0ltpnf	|- 0 < +oo
61		ubioc1	|- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> +oo e. ( 0 (,] +oo ) )
62	7 9 60 61	mp3an	|- +oo e. ( 0 (,] +oo )
63	62	a1i	|- ( ( A e. J /\ +oo e. A ) -> +oo e. ( 0 (,] +oo ) )
64	59 63	elind	|- ( ( A e. J /\ +oo e. A ) -> +oo e. ( A i^i ( 0 (,] +oo ) ) )
65		pnfnei	|- ( ( ( A i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) /\ +oo e. ( A i^i ( 0 (,] +oo ) ) ) -> E. y e. RR ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) )
66	58 64 65	syl2anc	|- ( ( A e. J /\ +oo e. A ) -> E. y e. RR ( y (,] +oo ) C_ ( A i^i ( 0 (,] +oo ) ) )
67	29 66	r19.29a	|- ( ( A e. J /\ +oo e. A ) -> E. x e. RR ( x (,] +oo ) C_ A )