Metamath Proof Explorer

Theorem leordtval2

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

Ref Expression
Hypotheses leordtval.1 ⊢A=ran⁡x∈ℝ*⟼x+∞
leordtval.2 ⊢B=ran⁡x∈ℝ*⟼−∞x
Assertion leordtval2 ⊢ordTop⁡≤=topGen⁡fi⁡A∪B

Proof

Step Hyp Ref Expression
1 leordtval.1 ⊢A=ran⁡x∈ℝ*⟼x+∞
2 leordtval.2 ⊢B=ran⁡x∈ℝ*⟼−∞x
3 letsr ⊢≤∈TosetRel
4 ledm ⊢ℝ*=dom⁡≤
5 1 leordtvallem1 ⊢A=ran⁡x∈ℝ*⟼y∈ℝ*|¬y≤x
6 1 2 leordtvallem2 ⊢B=ran⁡x∈ℝ*⟼y∈ℝ*|¬x≤y
7 4 5 6 ordtval ⊢≤∈TosetRel→ordTop⁡≤=topGen⁡fi⁡ℝ*∪A∪B
8 3 7 ax-mp ⊢ordTop⁡≤=topGen⁡fi⁡ℝ*∪A∪B
9 snex ⊢ℝ*∈V
10 xrex ⊢ℝ*∈V
11 10 pwex ⊢𝒫ℝ*∈V
12 eqid ⊢x∈ℝ*⟼x+∞=x∈ℝ*⟼x+∞
13 iocssxr ⊢x+∞⊆ℝ*
14 10 13 elpwi2 ⊢x+∞∈𝒫ℝ*
15 14 a1i ⊢x∈ℝ*→x+∞∈𝒫ℝ*
16 12 15 fmpti ⊢x∈ℝ*⟼x+∞:ℝ*⟶𝒫ℝ*
17 frn ⊢x∈ℝ*⟼x+∞:ℝ*⟶𝒫ℝ*→ran⁡x∈ℝ*⟼x+∞⊆𝒫ℝ*
18 16 17 ax-mp ⊢ran⁡x∈ℝ*⟼x+∞⊆𝒫ℝ*
19 1 18 eqsstri ⊢A⊆𝒫ℝ*
20 eqid ⊢x∈ℝ*⟼−∞x=x∈ℝ*⟼−∞x
21 icossxr ⊢−∞x⊆ℝ*
22 10 21 elpwi2 ⊢−∞x∈𝒫ℝ*
23 22 a1i ⊢x∈ℝ*→−∞x∈𝒫ℝ*
24 20 23 fmpti ⊢x∈ℝ*⟼−∞x:ℝ*⟶𝒫ℝ*
25 frn ⊢x∈ℝ*⟼−∞x:ℝ*⟶𝒫ℝ*→ran⁡x∈ℝ*⟼−∞x⊆𝒫ℝ*
26 24 25 ax-mp ⊢ran⁡x∈ℝ*⟼−∞x⊆𝒫ℝ*
27 2 26 eqsstri ⊢B⊆𝒫ℝ*
28 19 27 unssi ⊢A∪B⊆𝒫ℝ*
29 11 28 ssexi ⊢A∪B∈V
30 9 29 unex ⊢ℝ*∪A∪B∈V
31 ssun2 ⊢A∪B⊆ℝ*∪A∪B
32 fiss ⊢ℝ*∪A∪B∈V∧A∪B⊆ℝ*∪A∪B→fi⁡A∪B⊆fi⁡ℝ*∪A∪B
33 30 31 32 mp2an ⊢fi⁡A∪B⊆fi⁡ℝ*∪A∪B
34 fvex ⊢topGen⁡fi⁡A∪B∈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 ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x≤z∧z≤y
47 df-ioc ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x<z∧z≤y
48 xrltnle ⊢0∈ℝ*∧w∈ℝ*→0<w↔¬w≤0
49 xrletr ⊢w∈ℝ*∧0∈ℝ*∧+∞∈ℝ*→w≤0∧0≤+∞→w≤+∞
50 xrlttr ⊢−∞∈ℝ*∧0∈ℝ*∧w∈ℝ*→−∞<0∧0<w→−∞<w
51 xrltle ⊢−∞∈ℝ*∧w∈ℝ*→−∞<w→−∞≤w
52 51 3adant2 ⊢−∞∈ℝ*∧0∈ℝ*∧w∈ℝ*→−∞<w→−∞≤w
53 50 52 syld ⊢−∞∈ℝ*∧0∈ℝ*∧w∈ℝ*→−∞<0∧0<w→−∞≤w
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 ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x≤z∧z<y
60 xrlelttr ⊢w∈ℝ*∧0∈ℝ*∧1∈ℝ*→w≤0∧0<1→w<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⁡A∪B∈V
72 ssun1 ⊢A⊆A∪B
73 eqid ⊢0+∞=0+∞
74 oveq1 ⊢x=0→x+∞=0+∞
75 74 rspceeqv ⊢0∈ℝ*∧0+∞=0+∞→∃x∈ℝ*0+∞=x+∞
76 42 73 75 mp2an ⊢∃x∈ℝ*0+∞=x+∞
77 ovex ⊢x+∞∈V
78 12 77 elrnmpti ⊢0+∞∈ran⁡x∈ℝ*⟼x+∞↔∃x∈ℝ*0+∞=x+∞
79 76 78 mpbir ⊢0+∞∈ran⁡x∈ℝ*⟼x+∞
80 79 1 eleqtrri ⊢0+∞∈A
81 72 80 sselii ⊢0+∞∈A∪B
82 ssun2 ⊢B⊆A∪B
83 eqid ⊢−∞1=−∞1
84 oveq2 ⊢x=1→−∞x=−∞1
85 84 rspceeqv ⊢1∈ℝ*∧−∞1=−∞1→∃x∈ℝ*−∞1=−∞x
86 57 83 85 mp2an ⊢∃x∈ℝ*−∞1=−∞x
87 ovex ⊢−∞x∈V
88 20 87 elrnmpti ⊢−∞1∈ran⁡x∈ℝ*⟼−∞x↔∃x∈ℝ*−∞1=−∞x
89 86 88 mpbir ⊢−∞1∈ran⁡x∈ℝ*⟼−∞x
90 89 2 eleqtrri ⊢−∞1∈B
91 82 90 sselii ⊢−∞1∈A∪B
92 prssi ⊢0+∞∈A∪B∧−∞1∈A∪B→0+∞−∞1⊆A∪B
93 81 91 92 mp2an ⊢0+∞−∞1⊆A∪B
94 ssfii ⊢A∪B∈V→A∪B⊆fi⁡A∪B
95 29 94 ax-mp ⊢A∪B⊆fi⁡A∪B
96 93 95 sstri ⊢0+∞−∞1⊆fi⁡A∪B
97 eltg3i ⊢fi⁡A∪B∈V∧0+∞−∞1⊆fi⁡A∪B→⋃0+∞−∞1∈topGen⁡fi⁡A∪B
98 71 96 97 mp2an ⊢⋃0+∞−∞1∈topGen⁡fi⁡A∪B
99 70 98 eqeltrri ⊢ℝ*∈topGen⁡fi⁡A∪B
100 snssi ⊢ℝ*∈topGen⁡fi⁡A∪B→ℝ*⊆topGen⁡fi⁡A∪B
101 99 100 ax-mp ⊢ℝ*⊆topGen⁡fi⁡A∪B
102 bastg ⊢fi⁡A∪B∈V→fi⁡A∪B⊆topGen⁡fi⁡A∪B
103 71 102 ax-mp ⊢fi⁡A∪B⊆topGen⁡fi⁡A∪B
104 95 103 sstri ⊢A∪B⊆topGen⁡fi⁡A∪B
105 101 104 unssi ⊢ℝ*∪A∪B⊆topGen⁡fi⁡A∪B
106 fiss ⊢topGen⁡fi⁡A∪B∈V∧ℝ*∪A∪B⊆topGen⁡fi⁡A∪B→fi⁡ℝ*∪A∪B⊆fi⁡topGen⁡fi⁡A∪B
107 34 105 106 mp2an ⊢fi⁡ℝ*∪A∪B⊆fi⁡topGen⁡fi⁡A∪B
108 fibas ⊢fi⁡A∪B∈TopBases
109 tgcl ⊢fi⁡A∪B∈TopBases→topGen⁡fi⁡A∪B∈Top
110 fitop ⊢topGen⁡fi⁡A∪B∈Top→fi⁡topGen⁡fi⁡A∪B=topGen⁡fi⁡A∪B
111 108 109 110 mp2b ⊢fi⁡topGen⁡fi⁡A∪B=topGen⁡fi⁡A∪B
112 107 111 sseqtri ⊢fi⁡ℝ*∪A∪B⊆topGen⁡fi⁡A∪B
113 2basgen ⊢fi⁡A∪B⊆fi⁡ℝ*∪A∪B∧fi⁡ℝ*∪A∪B⊆topGen⁡fi⁡A∪B→topGen⁡fi⁡A∪B=topGen⁡fi⁡ℝ*∪A∪B
114 33 112 113 mp2an ⊢topGen⁡fi⁡A∪B=topGen⁡fi⁡ℝ*∪A∪B
115 8 114 eqtr4i ⊢ordTop⁡≤=topGen⁡fi⁡A∪B