Metamath Proof Explorer

Theorem 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 df-ss ⊢ ( 𝑣 ⊆ ℝ ↔ ( 𝑣 ∩ ℝ ) = 𝑣 )
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 (,) ) = 𝐽