xrtgioo

Description: The topology on the extended reals coincides with the standard topology on the reals, when restricted to RR . (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Hypothesis	xrtgioo.1	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾_t ℝ )
	Assertion	xrtgioo	⊢ ( topGen ‘ ran (,) ) = 𝐽

Proof

Step	Hyp	Ref	Expression
1		xrtgioo.1	⊢ 𝐽 = ( ( ordTop ‘ ≤ ) ↾_t ℝ )
2		letop	⊢ ( ordTop ‘ ≤ ) ∈ Top
3		ioof	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ
4		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ^* × ℝ^* ) )
5	3 4	ax-mp	⊢ (,) Fn ( ℝ^* × ℝ^* )
6		iooordt	⊢ ( 𝑥 (,) 𝑦 ) ∈ ( ordTop ‘ ≤ )
7	6	rgen2w	⊢ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* ( 𝑥 (,) 𝑦 ) ∈ ( ordTop ‘ ≤ )
8		ffnov	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ ( ordTop ‘ ≤ ) ↔ ( (,) Fn ( ℝ^* × ℝ^* ) ∧ ∀ 𝑥 ∈ ℝ^* ∀ 𝑦 ∈ ℝ^* ( 𝑥 (,) 𝑦 ) ∈ ( ordTop ‘ ≤ ) ) )
9	5 7 8	mpbir2an	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ ( ordTop ‘ ≤ )
10		frn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ ( ordTop ‘ ≤ ) → ran (,) ⊆ ( ordTop ‘ ≤ ) )
11	9 10	ax-mp	⊢ ran (,) ⊆ ( ordTop ‘ ≤ )
12		tgss	⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ ran (,) ⊆ ( ordTop ‘ ≤ ) ) → ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ ( ordTop ‘ ≤ ) ) )
13	2 11 12	mp2an	⊢ ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ ( ordTop ‘ ≤ ) )
14		tgtop	⊢ ( ( ordTop ‘ ≤ ) ∈ Top → ( topGen ‘ ( ordTop ‘ ≤ ) ) = ( ordTop ‘ ≤ ) )
15	2 14	ax-mp	⊢ ( topGen ‘ ( ordTop ‘ ≤ ) ) = ( ordTop ‘ ≤ )
16	13 15	sseqtri	⊢ ( topGen ‘ ran (,) ) ⊆ ( ordTop ‘ ≤ )
17	16	sseli	⊢ ( 𝑥 ∈ ( topGen ‘ ran (,) ) → 𝑥 ∈ ( ordTop ‘ ≤ ) )
18		retopon	⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
19		toponss	⊢ ( ( ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ ) ∧ 𝑥 ∈ ( topGen ‘ ran (,) ) ) → 𝑥 ⊆ ℝ )
20	18 19	mpan	⊢ ( 𝑥 ∈ ( topGen ‘ ran (,) ) → 𝑥 ⊆ ℝ )
21		reordt	⊢ ℝ ∈ ( ordTop ‘ ≤ )
22		restopn2	⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ ℝ ∈ ( ordTop ‘ ≤ ) ) → ( 𝑥 ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) ↔ ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑥 ⊆ ℝ ) ) )
23	2 21 22	mp2an	⊢ ( 𝑥 ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) ↔ ( 𝑥 ∈ ( ordTop ‘ ≤ ) ∧ 𝑥 ⊆ ℝ ) )
24	17 20 23	sylanbrc	⊢ ( 𝑥 ∈ ( topGen ‘ ran (,) ) → 𝑥 ∈ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) )
25	24	ssriv	⊢ ( topGen ‘ ran (,) ) ⊆ ( ( ordTop ‘ ≤ ) ↾_t ℝ )
26		eqid	⊢ ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) = ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) )
27		eqid	⊢ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) = ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) )
28		eqid	⊢ ran (,) = ran (,)
29	26 27 28	leordtval	⊢ ( ordTop ‘ ≤ ) = ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) )
30	29	oveq1i	⊢ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) = ( ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ↾_t ℝ )
31	29 2	eqeltrri	⊢ ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ∈ Top
32		tgclb	⊢ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases ↔ ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ∈ Top )
33	31 32	mpbir	⊢ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases
34		reex	⊢ ℝ ∈ V
35		tgrest	⊢ ( ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases ∧ ℝ ∈ V ) → ( topGen ‘ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ) = ( ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ↾_t ℝ ) )
36	33 34 35	mp2an	⊢ ( topGen ‘ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ) = ( ( topGen ‘ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ) ↾_t ℝ )
37	30 36	eqtr4i	⊢ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) = ( topGen ‘ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) )
38		retopbas	⊢ ran (,) ∈ TopBases
39		elrest	⊢ ( ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ∈ TopBases ∧ ℝ ∈ V ) → ( 𝑢 ∈ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ↔ ∃ 𝑣 ∈ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) 𝑢 = ( 𝑣 ∩ ℝ ) ) )
40	33 34 39	mp2an	⊢ ( 𝑢 ∈ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ↔ ∃ 𝑣 ∈ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) 𝑢 = ( 𝑣 ∩ ℝ ) )
41		elun	⊢ ( 𝑣 ∈ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↔ ( 𝑣 ∈ ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∨ 𝑣 ∈ ran (,) ) )
42		elun	⊢ ( 𝑣 ∈ ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ↔ ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∨ 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) )
43		eqid	⊢ ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) = ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) )
44	43	elrnmpt	⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ↔ ∃ 𝑥 ∈ ℝ^* 𝑣 = ( 𝑥 (,] +∞ ) ) )
45	44	elv	⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ↔ ∃ 𝑥 ∈ ℝ^* 𝑣 = ( 𝑥 (,] +∞ ) )
46		simpl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → 𝑥 ∈ ℝ^* )
47		pnfxr	⊢ +∞ ∈ ℝ^*
48	47	a1i	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → +∞ ∈ ℝ^* )
49		rexr	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ^* )
50	49	adantl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ^* )
51		df-ioc	⊢ (,] = ( 𝑎 ∈ ℝ^* , 𝑏 ∈ ℝ^* ↦ { 𝑐 ∈ ℝ^* ∣ ( 𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏 ) } )
52	51	elixx3g	⊢ ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ( ( 𝑥 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ ( 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
53	52	baib	⊢ ( ( 𝑥 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ( 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
54	46 48 50 53	syl3anc	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ( 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
55		pnfge	⊢ ( 𝑦 ∈ ℝ^* → 𝑦 ≤ +∞ )
56	50 55	syl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → 𝑦 ≤ +∞ )
57	56	biantrud	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ ( 𝑥 < 𝑦 ∧ 𝑦 ≤ +∞ ) ) )
58		ltpnf	⊢ ( 𝑦 ∈ ℝ → 𝑦 < +∞ )
59	58	adantl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → 𝑦 < +∞ )
60	59	biantrud	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑥 < 𝑦 ↔ ( 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) )
61	54 57 60	3bitr2d	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ↔ ( 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) )
62	61	pm5.32da	⊢ ( 𝑥 ∈ ℝ^* → ( ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ ( 𝑥 (,] +∞ ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) ) )
63		elin	⊢ ( 𝑦 ∈ ( ( 𝑥 (,] +∞ ) ∩ ℝ ) ↔ ( 𝑦 ∈ ( 𝑥 (,] +∞ ) ∧ 𝑦 ∈ ℝ ) )
64	63	biancomi	⊢ ( 𝑦 ∈ ( ( 𝑥 (,] +∞ ) ∩ ℝ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ ( 𝑥 (,] +∞ ) ) )
65		3anass	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ ( 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) )
66	62 64 65	3bitr4g	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑦 ∈ ( ( 𝑥 (,] +∞ ) ∩ ℝ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) )
67		elioo2	⊢ ( ( 𝑥 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ) → ( 𝑦 ∈ ( 𝑥 (,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) )
68	47 67	mpan2	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑦 ∈ ( 𝑥 (,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 < 𝑦 ∧ 𝑦 < +∞ ) ) )
69	66 68	bitr4d	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑦 ∈ ( ( 𝑥 (,] +∞ ) ∩ ℝ ) ↔ 𝑦 ∈ ( 𝑥 (,) +∞ ) ) )
70	69	eqrdv	⊢ ( 𝑥 ∈ ℝ^* → ( ( 𝑥 (,] +∞ ) ∩ ℝ ) = ( 𝑥 (,) +∞ ) )
71		ioorebas	⊢ ( 𝑥 (,) +∞ ) ∈ ran (,)
72	70 71	eqeltrdi	⊢ ( 𝑥 ∈ ℝ^* → ( ( 𝑥 (,] +∞ ) ∩ ℝ ) ∈ ran (,) )
73		ineq1	⊢ ( 𝑣 = ( 𝑥 (,] +∞ ) → ( 𝑣 ∩ ℝ ) = ( ( 𝑥 (,] +∞ ) ∩ ℝ ) )
74	73	eleq1d	⊢ ( 𝑣 = ( 𝑥 (,] +∞ ) → ( ( 𝑣 ∩ ℝ ) ∈ ran (,) ↔ ( ( 𝑥 (,] +∞ ) ∩ ℝ ) ∈ ran (,) ) )
75	72 74	syl5ibrcom	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑣 = ( 𝑥 (,] +∞ ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) ) )
76	75	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℝ^* 𝑣 = ( 𝑥 (,] +∞ ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
77	45 76	sylbi	⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
78		eqid	⊢ ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) = ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) )
79	78	elrnmpt	⊢ ( 𝑣 ∈ V → ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ↔ ∃ 𝑥 ∈ ℝ^* 𝑣 = ( -∞ [,) 𝑥 ) ) )
80	79	elv	⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ↔ ∃ 𝑥 ∈ ℝ^* 𝑣 = ( -∞ [,) 𝑥 ) )
81		mnfxr	⊢ -∞ ∈ ℝ^*
82	81	a1i	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → -∞ ∈ ℝ^* )
83		df-ico	⊢ [,) = ( 𝑎 ∈ ℝ^* , 𝑏 ∈ ℝ^* ↦ { 𝑐 ∈ ℝ^* ∣ ( 𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏 ) } )
84	83	elixx3g	⊢ ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ( ( -∞ ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) ∧ ( -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
85	84	baib	⊢ ( ( -∞ ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ^* ) → ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ( -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
86	82 46 50 85	syl3anc	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ( -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
87		mnfle	⊢ ( 𝑦 ∈ ℝ^* → -∞ ≤ 𝑦 )
88	50 87	syl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → -∞ ≤ 𝑦 )
89	88	biantrurd	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ ( -∞ ≤ 𝑦 ∧ 𝑦 < 𝑥 ) ) )
90		mnflt	⊢ ( 𝑦 ∈ ℝ → -∞ < 𝑦 )
91	90	adantl	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → -∞ < 𝑦 )
92	91	biantrurd	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑦 < 𝑥 ↔ ( -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) )
93	86 89 92	3bitr2d	⊢ ( ( 𝑥 ∈ ℝ^* ∧ 𝑦 ∈ ℝ ) → ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ↔ ( -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) )
94	93	pm5.32da	⊢ ( 𝑥 ∈ ℝ^* → ( ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ ( -∞ [,) 𝑥 ) ) ↔ ( 𝑦 ∈ ℝ ∧ ( -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) ) )
95		elin	⊢ ( 𝑦 ∈ ( ( -∞ [,) 𝑥 ) ∩ ℝ ) ↔ ( 𝑦 ∈ ( -∞ [,) 𝑥 ) ∧ 𝑦 ∈ ℝ ) )
96	95	biancomi	⊢ ( 𝑦 ∈ ( ( -∞ [,) 𝑥 ) ∩ ℝ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑦 ∈ ( -∞ [,) 𝑥 ) ) )
97		3anass	⊢ ( ( 𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ↔ ( 𝑦 ∈ ℝ ∧ ( -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) )
98	94 96 97	3bitr4g	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑦 ∈ ( ( -∞ [,) 𝑥 ) ∩ ℝ ) ↔ ( 𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) )
99		elioo2	⊢ ( ( -∞ ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( 𝑦 ∈ ( -∞ (,) 𝑥 ) ↔ ( 𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) )
100	81 99	mpan	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑦 ∈ ( -∞ (,) 𝑥 ) ↔ ( 𝑦 ∈ ℝ ∧ -∞ < 𝑦 ∧ 𝑦 < 𝑥 ) ) )
101	98 100	bitr4d	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑦 ∈ ( ( -∞ [,) 𝑥 ) ∩ ℝ ) ↔ 𝑦 ∈ ( -∞ (,) 𝑥 ) ) )
102	101	eqrdv	⊢ ( 𝑥 ∈ ℝ^* → ( ( -∞ [,) 𝑥 ) ∩ ℝ ) = ( -∞ (,) 𝑥 ) )
103		ioorebas	⊢ ( -∞ (,) 𝑥 ) ∈ ran (,)
104	102 103	eqeltrdi	⊢ ( 𝑥 ∈ ℝ^* → ( ( -∞ [,) 𝑥 ) ∩ ℝ ) ∈ ran (,) )
105		ineq1	⊢ ( 𝑣 = ( -∞ [,) 𝑥 ) → ( 𝑣 ∩ ℝ ) = ( ( -∞ [,) 𝑥 ) ∩ ℝ ) )
106	105	eleq1d	⊢ ( 𝑣 = ( -∞ [,) 𝑥 ) → ( ( 𝑣 ∩ ℝ ) ∈ ran (,) ↔ ( ( -∞ [,) 𝑥 ) ∩ ℝ ) ∈ ran (,) ) )
107	104 106	syl5ibrcom	⊢ ( 𝑥 ∈ ℝ^* → ( 𝑣 = ( -∞ [,) 𝑥 ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) ) )
108	107	rexlimiv	⊢ ( ∃ 𝑥 ∈ ℝ^* 𝑣 = ( -∞ [,) 𝑥 ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
109	80 108	sylbi	⊢ ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
110	77 109	jaoi	⊢ ( ( 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∨ 𝑣 ∈ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
111	42 110	sylbi	⊢ ( 𝑣 ∈ ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
112		elssuni	⊢ ( 𝑣 ∈ ran (,) → 𝑣 ⊆ ∪ ran (,) )
113		unirnioo	⊢ ℝ = ∪ ran (,)
114	112 113	sseqtrrdi	⊢ ( 𝑣 ∈ ran (,) → 𝑣 ⊆ ℝ )
115		dfss2	⊢ ( 𝑣 ⊆ ℝ ↔ ( 𝑣 ∩ ℝ ) = 𝑣 )
116	114 115	sylib	⊢ ( 𝑣 ∈ ran (,) → ( 𝑣 ∩ ℝ ) = 𝑣 )
117		id	⊢ ( 𝑣 ∈ ran (,) → 𝑣 ∈ ran (,) )
118	116 117	eqeltrd	⊢ ( 𝑣 ∈ ran (,) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
119	111 118	jaoi	⊢ ( ( 𝑣 ∈ ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∨ 𝑣 ∈ ran (,) ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
120	41 119	sylbi	⊢ ( 𝑣 ∈ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) → ( 𝑣 ∩ ℝ ) ∈ ran (,) )
121		eleq1	⊢ ( 𝑢 = ( 𝑣 ∩ ℝ ) → ( 𝑢 ∈ ran (,) ↔ ( 𝑣 ∩ ℝ ) ∈ ran (,) ) )
122	120 121	syl5ibrcom	⊢ ( 𝑣 ∈ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) → ( 𝑢 = ( 𝑣 ∩ ℝ ) → 𝑢 ∈ ran (,) ) )
123	122	rexlimiv	⊢ ( ∃ 𝑣 ∈ ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) 𝑢 = ( 𝑣 ∩ ℝ ) → 𝑢 ∈ ran (,) )
124	40 123	sylbi	⊢ ( 𝑢 ∈ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) → 𝑢 ∈ ran (,) )
125	124	ssriv	⊢ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ⊆ ran (,)
126		tgss	⊢ ( ( ran (,) ∈ TopBases ∧ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ⊆ ran (,) ) → ( topGen ‘ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ) ⊆ ( topGen ‘ ran (,) ) )
127	38 125 126	mp2an	⊢ ( topGen ‘ ( ( ( ran ( 𝑥 ∈ ℝ^* ↦ ( 𝑥 (,] +∞ ) ) ∪ ran ( 𝑥 ∈ ℝ^* ↦ ( -∞ [,) 𝑥 ) ) ) ∪ ran (,) ) ↾_t ℝ ) ) ⊆ ( topGen ‘ ran (,) )
128	37 127	eqsstri	⊢ ( ( ordTop ‘ ≤ ) ↾_t ℝ ) ⊆ ( topGen ‘ ran (,) )
129	25 128	eqssi	⊢ ( topGen ‘ ran (,) ) = ( ( ordTop ‘ ≤ ) ↾_t ℝ )
130	129 1	eqtr4i	⊢ ( topGen ‘ ran (,) ) = 𝐽

Metamath Proof Explorer

Theorem xrtgioo

Proof