Step | Hyp | Ref
| Expression |
1 | | letsr 17966 |
. . 3
⊢ ≤
∈ TosetRel |
2 | | ledm 17963 |
. . . 4
⊢
ℝ* = dom ≤ |
3 | | leordtval.1 |
. . . . 5
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
4 | 3 | leordtvallem1 21974 |
. . . 4
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ*
∣ ¬ 𝑦 ≤ 𝑥}) |
5 | | leordtval.2 |
. . . . 5
⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
6 | 3, 5 | leordtvallem2 21975 |
. . . 4
⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ*
∣ ¬ 𝑥 ≤ 𝑦}) |
7 | 2, 4, 6 | ordtval 21953 |
. . 3
⊢ ( ≤
∈ TosetRel → (ordTop‘ ≤ ) =
(topGen‘(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))))) |
8 | 1, 7 | ax-mp 5 |
. 2
⊢
(ordTop‘ ≤ ) = (topGen‘(fi‘({ℝ*}
∪ (𝐴 ∪ 𝐵)))) |
9 | | snex 5308 |
. . . . 5
⊢
{ℝ*} ∈ V |
10 | | xrex 12482 |
. . . . . . 7
⊢
ℝ* ∈ V |
11 | 10 | pwex 5257 |
. . . . . 6
⊢ 𝒫
ℝ* ∈ V |
12 | | eqid 2739 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)) =
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) |
13 | | iocssxr 12918 |
. . . . . . . . . . . 12
⊢ (𝑥(,]+∞) ⊆
ℝ* |
14 | 10, 13 | elpwi2 5224 |
. . . . . . . . . . 11
⊢ (𝑥(,]+∞) ∈ 𝒫
ℝ* |
15 | 14 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ (𝑥(,]+∞)
∈ 𝒫 ℝ*) |
16 | 12, 15 | fmpti 6899 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)):ℝ*⟶𝒫
ℝ* |
17 | | frn 6522 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)):ℝ*⟶𝒫
ℝ* → ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ⊆ 𝒫
ℝ*) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ⊆ 𝒫
ℝ* |
19 | 3, 18 | eqsstri 3921 |
. . . . . . 7
⊢ 𝐴 ⊆ 𝒫
ℝ* |
20 | | eqid 2739 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)) =
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) |
21 | | icossxr 12919 |
. . . . . . . . . . . 12
⊢
(-∞[,)𝑥)
⊆ ℝ* |
22 | 10, 21 | elpwi2 5224 |
. . . . . . . . . . 11
⊢
(-∞[,)𝑥)
∈ 𝒫 ℝ* |
23 | 22 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ (-∞[,)𝑥)
∈ 𝒫 ℝ*) |
24 | 20, 23 | fmpti 6899 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)):ℝ*⟶𝒫
ℝ* |
25 | | frn 6522 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)):ℝ*⟶𝒫
ℝ* → ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ⊆
𝒫 ℝ*) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) ⊆ 𝒫
ℝ* |
27 | 5, 26 | eqsstri 3921 |
. . . . . . 7
⊢ 𝐵 ⊆ 𝒫
ℝ* |
28 | 19, 27 | unssi 4085 |
. . . . . 6
⊢ (𝐴 ∪ 𝐵) ⊆ 𝒫
ℝ* |
29 | 11, 28 | ssexi 5200 |
. . . . 5
⊢ (𝐴 ∪ 𝐵) ∈ V |
30 | 9, 29 | unex 7500 |
. . . 4
⊢
({ℝ*} ∪ (𝐴 ∪ 𝐵)) ∈ V |
31 | | ssun2 4073 |
. . . 4
⊢ (𝐴 ∪ 𝐵) ⊆ ({ℝ*} ∪
(𝐴 ∪ 𝐵)) |
32 | | fiss 8974 |
. . . 4
⊢
((({ℝ*} ∪ (𝐴 ∪ 𝐵)) ∈ V ∧ (𝐴 ∪ 𝐵) ⊆ ({ℝ*} ∪
(𝐴 ∪ 𝐵))) → (fi‘(𝐴 ∪ 𝐵)) ⊆ (fi‘({ℝ*}
∪ (𝐴 ∪ 𝐵)))) |
33 | 30, 31, 32 | mp2an 692 |
. . 3
⊢
(fi‘(𝐴 ∪
𝐵)) ⊆
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) |
34 | | fvex 6700 |
. . . . 5
⊢
(topGen‘(fi‘(𝐴 ∪ 𝐵))) ∈ V |
35 | | ovex 7216 |
. . . . . . . . . 10
⊢
(0(,]+∞) ∈ V |
36 | | ovex 7216 |
. . . . . . . . . 10
⊢
(-∞[,)1) ∈ V |
37 | 35, 36 | unipr 4824 |
. . . . . . . . 9
⊢ ∪ {(0(,]+∞), (-∞[,)1)} = ((0(,]+∞) ∪
(-∞[,)1)) |
38 | | iocssxr 12918 |
. . . . . . . . . . 11
⊢
(0(,]+∞) ⊆ ℝ* |
39 | | icossxr 12919 |
. . . . . . . . . . 11
⊢
(-∞[,)1) ⊆ ℝ* |
40 | 38, 39 | unssi 4085 |
. . . . . . . . . 10
⊢
((0(,]+∞) ∪ (-∞[,)1)) ⊆
ℝ* |
41 | | mnfxr 10789 |
. . . . . . . . . . . . 13
⊢ -∞
∈ ℝ* |
42 | | 0xr 10779 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
43 | | pnfxr 10786 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
44 | | mnflt0 12616 |
. . . . . . . . . . . . . 14
⊢ -∞
< 0 |
45 | | 0lepnf 12623 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
+∞ |
46 | | df-icc 12841 |
. . . . . . . . . . . . . . 15
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
47 | | df-ioc 12839 |
. . . . . . . . . . . . . . 15
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
48 | | xrltnle 10799 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (0 <
𝑤 ↔ ¬ 𝑤 ≤ 0)) |
49 | | xrletr 12647 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ*
∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 ≤ 0 ∧ 0
≤ +∞) → 𝑤
≤ +∞)) |
50 | | xrlttr 12629 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((-∞ < 0 ∧ 0 < 𝑤) → -∞ < 𝑤)) |
51 | | xrltle 12638 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-∞
< 𝑤 → -∞ ≤
𝑤)) |
52 | 51 | 3adant2 1132 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (-∞ < 𝑤 → -∞ ≤ 𝑤)) |
53 | 50, 52 | syld 47 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((-∞ < 0 ∧ 0 < 𝑤) → -∞ ≤ 𝑤)) |
54 | 46, 47, 48, 46, 49, 53 | ixxun 12850 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ ℝ* ∧ 0 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞
< 0 ∧ 0 ≤ +∞)) → ((-∞[,]0) ∪ (0(,]+∞)) =
(-∞[,]+∞)) |
55 | 44, 45, 54 | mpanr12 705 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((-∞[,]0) ∪
(0(,]+∞)) = (-∞[,]+∞)) |
56 | 41, 42, 43, 55 | mp3an 1462 |
. . . . . . . . . . . 12
⊢
((-∞[,]0) ∪ (0(,]+∞)) =
(-∞[,]+∞) |
57 | | 1xr 10791 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ* |
58 | | 0lt1 11253 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
59 | | df-ico 12840 |
. . . . . . . . . . . . . . 15
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
60 | | xrlelttr 12645 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ*
∧ 0 ∈ ℝ* ∧ 1 ∈ ℝ*) →
((𝑤 ≤ 0 ∧ 0 < 1)
→ 𝑤 <
1)) |
61 | 59, 46, 60 | ixxss2 12853 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ* ∧ 0 < 1) → (-∞[,]0) ⊆
(-∞[,)1)) |
62 | 57, 58, 61 | mp2an 692 |
. . . . . . . . . . . . 13
⊢
(-∞[,]0) ⊆ (-∞[,)1) |
63 | | unss1 4079 |
. . . . . . . . . . . . 13
⊢
((-∞[,]0) ⊆ (-∞[,)1) → ((-∞[,]0) ∪
(0(,]+∞)) ⊆ ((-∞[,)1) ∪ (0(,]+∞))) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((-∞[,]0) ∪ (0(,]+∞)) ⊆ ((-∞[,)1) ∪
(0(,]+∞)) |
65 | 56, 64 | eqsstrri 3922 |
. . . . . . . . . . 11
⊢
(-∞[,]+∞) ⊆ ((-∞[,)1) ∪
(0(,]+∞)) |
66 | | iccmax 12910 |
. . . . . . . . . . 11
⊢
(-∞[,]+∞) = ℝ* |
67 | | uncom 4053 |
. . . . . . . . . . 11
⊢
((-∞[,)1) ∪ (0(,]+∞)) = ((0(,]+∞) ∪
(-∞[,)1)) |
68 | 65, 66, 67 | 3sstr3i 3929 |
. . . . . . . . . 10
⊢
ℝ* ⊆ ((0(,]+∞) ∪
(-∞[,)1)) |
69 | 40, 68 | eqssi 3903 |
. . . . . . . . 9
⊢
((0(,]+∞) ∪ (-∞[,)1)) =
ℝ* |
70 | 37, 69 | eqtri 2762 |
. . . . . . . 8
⊢ ∪ {(0(,]+∞), (-∞[,)1)} =
ℝ* |
71 | | fvex 6700 |
. . . . . . . . 9
⊢
(fi‘(𝐴 ∪
𝐵)) ∈
V |
72 | | ssun1 4072 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
73 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(0(,]+∞) = (0(,]+∞) |
74 | | oveq1 7190 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝑥(,]+∞) =
(0(,]+∞)) |
75 | 74 | rspceeqv 3544 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ (0(,]+∞) = (0(,]+∞)) →
∃𝑥 ∈
ℝ* (0(,]+∞) = (𝑥(,]+∞)) |
76 | 42, 73, 75 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
∃𝑥 ∈
ℝ* (0(,]+∞) = (𝑥(,]+∞) |
77 | | ovex 7216 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(,]+∞) ∈
V |
78 | 12, 77 | elrnmpti 5813 |
. . . . . . . . . . . . . 14
⊢
((0(,]+∞) ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* (0(,]+∞) = (𝑥(,]+∞)) |
79 | 76, 78 | mpbir 234 |
. . . . . . . . . . . . 13
⊢
(0(,]+∞) ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
80 | 79, 3 | eleqtrri 2833 |
. . . . . . . . . . . 12
⊢
(0(,]+∞) ∈ 𝐴 |
81 | 72, 80 | sselii 3884 |
. . . . . . . . . . 11
⊢
(0(,]+∞) ∈ (𝐴 ∪ 𝐵) |
82 | | ssun2 4073 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
83 | | eqid 2739 |
. . . . . . . . . . . . . . 15
⊢
(-∞[,)1) = (-∞[,)1) |
84 | | oveq2 7191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → (-∞[,)𝑥) =
(-∞[,)1)) |
85 | 84 | rspceeqv 3544 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ* ∧ (-∞[,)1) = (-∞[,)1)) →
∃𝑥 ∈
ℝ* (-∞[,)1) = (-∞[,)𝑥)) |
86 | 57, 83, 85 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
∃𝑥 ∈
ℝ* (-∞[,)1) = (-∞[,)𝑥) |
87 | | ovex 7216 |
. . . . . . . . . . . . . . 15
⊢
(-∞[,)𝑥)
∈ V |
88 | 20, 87 | elrnmpti 5813 |
. . . . . . . . . . . . . 14
⊢
((-∞[,)1) ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* (-∞[,)1) = (-∞[,)𝑥)) |
89 | 86, 88 | mpbir 234 |
. . . . . . . . . . . . 13
⊢
(-∞[,)1) ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
90 | 89, 5 | eleqtrri 2833 |
. . . . . . . . . . . 12
⊢
(-∞[,)1) ∈ 𝐵 |
91 | 82, 90 | sselii 3884 |
. . . . . . . . . . 11
⊢
(-∞[,)1) ∈ (𝐴 ∪ 𝐵) |
92 | | prssi 4719 |
. . . . . . . . . . 11
⊢
(((0(,]+∞) ∈ (𝐴 ∪ 𝐵) ∧ (-∞[,)1) ∈ (𝐴 ∪ 𝐵)) → {(0(,]+∞), (-∞[,)1)}
⊆ (𝐴 ∪ 𝐵)) |
93 | 81, 91, 92 | mp2an 692 |
. . . . . . . . . 10
⊢
{(0(,]+∞), (-∞[,)1)} ⊆ (𝐴 ∪ 𝐵) |
94 | | ssfii 8969 |
. . . . . . . . . . 11
⊢ ((𝐴 ∪ 𝐵) ∈ V → (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵))) |
95 | 29, 94 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵)) |
96 | 93, 95 | sstri 3896 |
. . . . . . . . 9
⊢
{(0(,]+∞), (-∞[,)1)} ⊆ (fi‘(𝐴 ∪ 𝐵)) |
97 | | eltg3i 21725 |
. . . . . . . . 9
⊢
(((fi‘(𝐴 ∪
𝐵)) ∈ V ∧
{(0(,]+∞), (-∞[,)1)} ⊆ (fi‘(𝐴 ∪ 𝐵))) → ∪
{(0(,]+∞), (-∞[,)1)} ∈ (topGen‘(fi‘(𝐴 ∪ 𝐵)))) |
98 | 71, 96, 97 | mp2an 692 |
. . . . . . . 8
⊢ ∪ {(0(,]+∞), (-∞[,)1)} ∈
(topGen‘(fi‘(𝐴
∪ 𝐵))) |
99 | 70, 98 | eqeltrri 2831 |
. . . . . . 7
⊢
ℝ* ∈ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
100 | | snssi 4706 |
. . . . . . 7
⊢
(ℝ* ∈ (topGen‘(fi‘(𝐴 ∪ 𝐵))) → {ℝ*} ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) |
101 | 99, 100 | ax-mp 5 |
. . . . . 6
⊢
{ℝ*} ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
102 | | bastg 21730 |
. . . . . . . 8
⊢
((fi‘(𝐴 ∪
𝐵)) ∈ V →
(fi‘(𝐴 ∪ 𝐵)) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) |
103 | 71, 102 | ax-mp 5 |
. . . . . . 7
⊢
(fi‘(𝐴 ∪
𝐵)) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵))) |
104 | 95, 103 | sstri 3896 |
. . . . . 6
⊢ (𝐴 ∪ 𝐵) ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
105 | 101, 104 | unssi 4085 |
. . . . 5
⊢
({ℝ*} ∪ (𝐴 ∪ 𝐵)) ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
106 | | fiss 8974 |
. . . . 5
⊢
(((topGen‘(fi‘(𝐴 ∪ 𝐵))) ∈ V ∧ ({ℝ*}
∪ (𝐴 ∪ 𝐵)) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) →
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ⊆
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵))))) |
107 | 34, 105, 106 | mp2an 692 |
. . . 4
⊢
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ⊆
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵)))) |
108 | | fibas 21741 |
. . . . 5
⊢
(fi‘(𝐴 ∪
𝐵)) ∈
TopBases |
109 | | tgcl 21733 |
. . . . 5
⊢
((fi‘(𝐴 ∪
𝐵)) ∈ TopBases →
(topGen‘(fi‘(𝐴
∪ 𝐵))) ∈
Top) |
110 | | fitop 21664 |
. . . . 5
⊢
((topGen‘(fi‘(𝐴 ∪ 𝐵))) ∈ Top →
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵)))) = (topGen‘(fi‘(𝐴 ∪ 𝐵)))) |
111 | 108, 109,
110 | mp2b 10 |
. . . 4
⊢
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵)))) = (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
112 | 107, 111 | sseqtri 3923 |
. . 3
⊢
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
113 | | 2basgen 21754 |
. . 3
⊢
(((fi‘(𝐴 ∪
𝐵)) ⊆
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ∧ (fi‘({ℝ*}
∪ (𝐴 ∪ 𝐵))) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) →
(topGen‘(fi‘(𝐴
∪ 𝐵))) =
(topGen‘(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))))) |
114 | 33, 112, 113 | mp2an 692 |
. 2
⊢
(topGen‘(fi‘(𝐴 ∪ 𝐵))) =
(topGen‘(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵)))) |
115 | 8, 114 | eqtr4i 2765 |
1
⊢
(ordTop‘ ≤ ) = (topGen‘(fi‘(𝐴 ∪ 𝐵))) |