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