# Metamath Proof Explorer

## Theorem leordtval2

Description: The topology of the extended reals. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses leordtval.1 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
leordtval.2 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
Assertion leordtval2 ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )

### Proof

Step Hyp Ref Expression
1 leordtval.1 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
2 leordtval.2 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
3 letsr ≤ ∈ TosetRel
4 ledm * = dom ≤
5 1 leordtvallem1 𝐴 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑦𝑥 } )
6 1 2 leordtvallem2 𝐵 = ran ( 𝑥 ∈ ℝ* ↦ { 𝑦 ∈ ℝ* ∣ ¬ 𝑥𝑦 } )
7 4 5 6 ordtval ( ≤ ∈ TosetRel → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ) )
8 3 7 ax-mp ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) )
9 snex { ℝ* } ∈ V
10 xrex * ∈ V
11 10 pwex 𝒫 ℝ* ∈ V
12 eqid ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) = ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
13 iocssxr ( 𝑥 (,] +∞ ) ⊆ ℝ*
14 10 13 elpwi2 ( 𝑥 (,] +∞ ) ∈ 𝒫 ℝ*
15 14 a1i ( 𝑥 ∈ ℝ* → ( 𝑥 (,] +∞ ) ∈ 𝒫 ℝ* )
16 12 15 fmpti ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) : ℝ* ⟶ 𝒫 ℝ*
17 frn ( ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) : ℝ* ⟶ 𝒫 ℝ* → ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ⊆ 𝒫 ℝ* )
18 16 17 ax-mp ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ⊆ 𝒫 ℝ*
19 1 18 eqsstri 𝐴 ⊆ 𝒫 ℝ*
20 eqid ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) = ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
21 icossxr ( -∞ [,) 𝑥 ) ⊆ ℝ*
22 10 21 elpwi2 ( -∞ [,) 𝑥 ) ∈ 𝒫 ℝ*
23 22 a1i ( 𝑥 ∈ ℝ* → ( -∞ [,) 𝑥 ) ∈ 𝒫 ℝ* )
24 20 23 fmpti ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) : ℝ* ⟶ 𝒫 ℝ*
25 frn ( ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) : ℝ* ⟶ 𝒫 ℝ* → ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ⊆ 𝒫 ℝ* )
26 24 25 ax-mp ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ⊆ 𝒫 ℝ*
27 2 26 eqsstri 𝐵 ⊆ 𝒫 ℝ*
28 19 27 unssi ( 𝐴𝐵 ) ⊆ 𝒫 ℝ*
29 11 28 ssexi ( 𝐴𝐵 ) ∈ V
30 9 29 unex ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ∈ V
31 ssun2 ( 𝐴𝐵 ) ⊆ ( { ℝ* } ∪ ( 𝐴𝐵 ) )
32 fiss ( ( ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ∈ V ∧ ( 𝐴𝐵 ) ⊆ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) → ( fi ‘ ( 𝐴𝐵 ) ) ⊆ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) )
33 30 31 32 mp2an ( fi ‘ ( 𝐴𝐵 ) ) ⊆ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) )
34 fvex ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ∈ V
35 ovex ( 0 (,] +∞ ) ∈ V
36 ovex ( -∞ [,) 1 ) ∈ V
37 35 36 unipr { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } = ( ( 0 (,] +∞ ) ∪ ( -∞ [,) 1 ) )
38 iocssxr ( 0 (,] +∞ ) ⊆ ℝ*
39 icossxr ( -∞ [,) 1 ) ⊆ ℝ*
40 38 39 unssi ( ( 0 (,] +∞ ) ∪ ( -∞ [,) 1 ) ) ⊆ ℝ*
41 mnfxr -∞ ∈ ℝ*
42 0xr 0 ∈ ℝ*
43 pnfxr +∞ ∈ ℝ*
44 mnflt0 -∞ < 0
45 0lepnf 0 ≤ +∞
46 df-icc [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧𝑦 ) } )
47 df-ioc (,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧𝑧𝑦 ) } )
48 xrltnle ( ( 0 ∈ ℝ*𝑤 ∈ ℝ* ) → ( 0 < 𝑤 ↔ ¬ 𝑤 ≤ 0 ) )
49 xrletr ( ( 𝑤 ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( 𝑤 ≤ 0 ∧ 0 ≤ +∞ ) → 𝑤 ≤ +∞ ) )
50 xrlttr ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ*𝑤 ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 < 𝑤 ) → -∞ < 𝑤 ) )
51 xrltle ( ( -∞ ∈ ℝ*𝑤 ∈ ℝ* ) → ( -∞ < 𝑤 → -∞ ≤ 𝑤 ) )
52 51 3adant2 ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ*𝑤 ∈ ℝ* ) → ( -∞ < 𝑤 → -∞ ≤ 𝑤 ) )
53 50 52 syld ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ*𝑤 ∈ ℝ* ) → ( ( -∞ < 0 ∧ 0 < 𝑤 ) → -∞ ≤ 𝑤 ) )
54 46 47 48 46 49 53 ixxun ( ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( -∞ < 0 ∧ 0 ≤ +∞ ) ) → ( ( -∞ [,] 0 ) ∪ ( 0 (,] +∞ ) ) = ( -∞ [,] +∞ ) )
55 44 45 54 mpanr12 ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( ( -∞ [,] 0 ) ∪ ( 0 (,] +∞ ) ) = ( -∞ [,] +∞ ) )
56 41 42 43 55 mp3an ( ( -∞ [,] 0 ) ∪ ( 0 (,] +∞ ) ) = ( -∞ [,] +∞ )
57 1xr 1 ∈ ℝ*
58 0lt1 0 < 1
59 df-ico [,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥𝑧𝑧 < 𝑦 ) } )
60 xrlelttr ( ( 𝑤 ∈ ℝ* ∧ 0 ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( 𝑤 ≤ 0 ∧ 0 < 1 ) → 𝑤 < 1 ) )
61 59 46 60 ixxss2 ( ( 1 ∈ ℝ* ∧ 0 < 1 ) → ( -∞ [,] 0 ) ⊆ ( -∞ [,) 1 ) )
62 57 58 61 mp2an ( -∞ [,] 0 ) ⊆ ( -∞ [,) 1 )
63 unss1 ( ( -∞ [,] 0 ) ⊆ ( -∞ [,) 1 ) → ( ( -∞ [,] 0 ) ∪ ( 0 (,] +∞ ) ) ⊆ ( ( -∞ [,) 1 ) ∪ ( 0 (,] +∞ ) ) )
64 62 63 ax-mp ( ( -∞ [,] 0 ) ∪ ( 0 (,] +∞ ) ) ⊆ ( ( -∞ [,) 1 ) ∪ ( 0 (,] +∞ ) )
65 56 64 eqsstrri ( -∞ [,] +∞ ) ⊆ ( ( -∞ [,) 1 ) ∪ ( 0 (,] +∞ ) )
66 iccmax ( -∞ [,] +∞ ) = ℝ*
67 uncom ( ( -∞ [,) 1 ) ∪ ( 0 (,] +∞ ) ) = ( ( 0 (,] +∞ ) ∪ ( -∞ [,) 1 ) )
68 65 66 67 3sstr3i * ⊆ ( ( 0 (,] +∞ ) ∪ ( -∞ [,) 1 ) )
69 40 68 eqssi ( ( 0 (,] +∞ ) ∪ ( -∞ [,) 1 ) ) = ℝ*
70 37 69 eqtri { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } = ℝ*
71 fvex ( fi ‘ ( 𝐴𝐵 ) ) ∈ V
72 ssun1 𝐴 ⊆ ( 𝐴𝐵 )
73 eqid ( 0 (,] +∞ ) = ( 0 (,] +∞ )
74 oveq1 ( 𝑥 = 0 → ( 𝑥 (,] +∞ ) = ( 0 (,] +∞ ) )
75 74 rspceeqv ( ( 0 ∈ ℝ* ∧ ( 0 (,] +∞ ) = ( 0 (,] +∞ ) ) → ∃ 𝑥 ∈ ℝ* ( 0 (,] +∞ ) = ( 𝑥 (,] +∞ ) )
76 42 73 75 mp2an 𝑥 ∈ ℝ* ( 0 (,] +∞ ) = ( 𝑥 (,] +∞ )
77 ovex ( 𝑥 (,] +∞ ) ∈ V
78 12 77 elrnmpti ( ( 0 (,] +∞ ) ∈ ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) ) ↔ ∃ 𝑥 ∈ ℝ* ( 0 (,] +∞ ) = ( 𝑥 (,] +∞ ) )
79 76 78 mpbir ( 0 (,] +∞ ) ∈ ran ( 𝑥 ∈ ℝ* ↦ ( 𝑥 (,] +∞ ) )
80 79 1 eleqtrri ( 0 (,] +∞ ) ∈ 𝐴
81 72 80 sselii ( 0 (,] +∞ ) ∈ ( 𝐴𝐵 )
82 ssun2 𝐵 ⊆ ( 𝐴𝐵 )
83 eqid ( -∞ [,) 1 ) = ( -∞ [,) 1 )
84 oveq2 ( 𝑥 = 1 → ( -∞ [,) 𝑥 ) = ( -∞ [,) 1 ) )
85 84 rspceeqv ( ( 1 ∈ ℝ* ∧ ( -∞ [,) 1 ) = ( -∞ [,) 1 ) ) → ∃ 𝑥 ∈ ℝ* ( -∞ [,) 1 ) = ( -∞ [,) 𝑥 ) )
86 57 83 85 mp2an 𝑥 ∈ ℝ* ( -∞ [,) 1 ) = ( -∞ [,) 𝑥 )
87 ovex ( -∞ [,) 𝑥 ) ∈ V
88 20 87 elrnmpti ( ( -∞ [,) 1 ) ∈ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) ) ↔ ∃ 𝑥 ∈ ℝ* ( -∞ [,) 1 ) = ( -∞ [,) 𝑥 ) )
89 86 88 mpbir ( -∞ [,) 1 ) ∈ ran ( 𝑥 ∈ ℝ* ↦ ( -∞ [,) 𝑥 ) )
90 89 2 eleqtrri ( -∞ [,) 1 ) ∈ 𝐵
91 82 90 sselii ( -∞ [,) 1 ) ∈ ( 𝐴𝐵 )
92 prssi ( ( ( 0 (,] +∞ ) ∈ ( 𝐴𝐵 ) ∧ ( -∞ [,) 1 ) ∈ ( 𝐴𝐵 ) ) → { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } ⊆ ( 𝐴𝐵 ) )
93 81 91 92 mp2an { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } ⊆ ( 𝐴𝐵 )
94 ssfii ( ( 𝐴𝐵 ) ∈ V → ( 𝐴𝐵 ) ⊆ ( fi ‘ ( 𝐴𝐵 ) ) )
95 29 94 ax-mp ( 𝐴𝐵 ) ⊆ ( fi ‘ ( 𝐴𝐵 ) )
96 93 95 sstri { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } ⊆ ( fi ‘ ( 𝐴𝐵 ) )
97 eltg3i ( ( ( fi ‘ ( 𝐴𝐵 ) ) ∈ V ∧ { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } ⊆ ( fi ‘ ( 𝐴𝐵 ) ) ) → { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } ∈ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) )
98 71 96 97 mp2an { ( 0 (,] +∞ ) , ( -∞ [,) 1 ) } ∈ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
99 70 98 eqeltrri * ∈ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
100 snssi ( ℝ* ∈ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) → { ℝ* } ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) )
101 99 100 ax-mp { ℝ* } ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
102 bastg ( ( fi ‘ ( 𝐴𝐵 ) ) ∈ V → ( fi ‘ ( 𝐴𝐵 ) ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) )
103 71 102 ax-mp ( fi ‘ ( 𝐴𝐵 ) ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
104 95 103 sstri ( 𝐴𝐵 ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
105 101 104 unssi ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
106 fiss ( ( ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ∈ V ∧ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ) → ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ⊆ ( fi ‘ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ) )
107 34 105 106 mp2an ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ⊆ ( fi ‘ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) )
108 fibas ( fi ‘ ( 𝐴𝐵 ) ) ∈ TopBases
109 tgcl ( ( fi ‘ ( 𝐴𝐵 ) ) ∈ TopBases → ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ∈ Top )
110 fitop ( ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ∈ Top → ( fi ‘ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ) = ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) )
111 108 109 110 mp2b ( fi ‘ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ) = ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
112 107 111 sseqtri ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )
113 2basgen ( ( ( fi ‘ ( 𝐴𝐵 ) ) ⊆ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ∧ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) ) → ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) = ( topGen ‘ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) ) )
114 33 112 113 mp2an ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) ) = ( topGen ‘ ( fi ‘ ( { ℝ* } ∪ ( 𝐴𝐵 ) ) ) )
115 8 114 eqtr4i ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( 𝐴𝐵 ) ) )