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 ‘ ( 𝐴 ∪ 𝐵 ) ) )