Step | Hyp | Ref
| Expression |
1 | | letsr 17050 |
. . 3
⊢ ≤
∈ TosetRel |
2 | | ledm 17047 |
. . . 4
⊢
ℝ* = dom ≤ |
3 | | leordtval.1 |
. . . . 5
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
4 | 3 | leordtvallem1 20824 |
. . . 4
⊢ 𝐴 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ*
∣ ¬ 𝑦 ≤ 𝑥}) |
5 | | leordtval.2 |
. . . . 5
⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
6 | 3, 5 | leordtvallem2 20825 |
. . . 4
⊢ 𝐵 = ran (𝑥 ∈ ℝ* ↦ {𝑦 ∈ ℝ*
∣ ¬ 𝑥 ≤ 𝑦}) |
7 | 2, 4, 6 | ordtval 20803 |
. . 3
⊢ ( ≤
∈ TosetRel → (ordTop‘ ≤ ) =
(topGen‘(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))))) |
8 | 1, 7 | ax-mp 5 |
. 2
⊢
(ordTop‘ ≤ ) = (topGen‘(fi‘({ℝ*}
∪ (𝐴 ∪ 𝐵)))) |
9 | | snex 4835 |
. . . . 5
⊢
{ℝ*} ∈ V |
10 | | xrex 11705 |
. . . . . . 7
⊢
ℝ* ∈ V |
11 | 10 | pwex 4774 |
. . . . . 6
⊢ 𝒫
ℝ* ∈ V |
12 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)) =
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) |
13 | | iocssxr 12128 |
. . . . . . . . . . . 12
⊢ (𝑥(,]+∞) ⊆
ℝ* |
14 | 10 | elpw2 4755 |
. . . . . . . . . . . 12
⊢ ((𝑥(,]+∞) ∈ 𝒫
ℝ* ↔ (𝑥(,]+∞) ⊆
ℝ*) |
15 | 13, 14 | mpbir 220 |
. . . . . . . . . . 11
⊢ (𝑥(,]+∞) ∈ 𝒫
ℝ* |
16 | 15 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ (𝑥(,]+∞)
∈ 𝒫 ℝ*) |
17 | 12, 16 | fmpti 6291 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)):ℝ*⟶𝒫
ℝ* |
18 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
↦ (𝑥(,]+∞)):ℝ*⟶𝒫
ℝ* → ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ⊆ 𝒫
ℝ*) |
19 | 17, 18 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝑥 ∈
ℝ* ↦ (𝑥(,]+∞)) ⊆ 𝒫
ℝ* |
20 | 3, 19 | eqsstri 3598 |
. . . . . . 7
⊢ 𝐴 ⊆ 𝒫
ℝ* |
21 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)) =
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) |
22 | | icossxr 12129 |
. . . . . . . . . . . 12
⊢
(-∞[,)𝑥)
⊆ ℝ* |
23 | 10 | elpw2 4755 |
. . . . . . . . . . . 12
⊢
((-∞[,)𝑥)
∈ 𝒫 ℝ* ↔ (-∞[,)𝑥) ⊆
ℝ*) |
24 | 22, 23 | mpbir 220 |
. . . . . . . . . . 11
⊢
(-∞[,)𝑥)
∈ 𝒫 ℝ* |
25 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ*
→ (-∞[,)𝑥)
∈ 𝒫 ℝ*) |
26 | 21, 25 | fmpti 6291 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)):ℝ*⟶𝒫
ℝ* |
27 | | frn 5966 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ*
↦ (-∞[,)𝑥)):ℝ*⟶𝒫
ℝ* → ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ⊆
𝒫 ℝ*) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . 8
⊢ ran
(𝑥 ∈
ℝ* ↦ (-∞[,)𝑥)) ⊆ 𝒫
ℝ* |
29 | 5, 28 | eqsstri 3598 |
. . . . . . 7
⊢ 𝐵 ⊆ 𝒫
ℝ* |
30 | 20, 29 | unssi 3750 |
. . . . . 6
⊢ (𝐴 ∪ 𝐵) ⊆ 𝒫
ℝ* |
31 | 11, 30 | ssexi 4731 |
. . . . 5
⊢ (𝐴 ∪ 𝐵) ∈ V |
32 | 9, 31 | unex 6854 |
. . . 4
⊢
({ℝ*} ∪ (𝐴 ∪ 𝐵)) ∈ V |
33 | | ssun2 3739 |
. . . 4
⊢ (𝐴 ∪ 𝐵) ⊆ ({ℝ*} ∪
(𝐴 ∪ 𝐵)) |
34 | | fiss 8213 |
. . . 4
⊢
((({ℝ*} ∪ (𝐴 ∪ 𝐵)) ∈ V ∧ (𝐴 ∪ 𝐵) ⊆ ({ℝ*} ∪
(𝐴 ∪ 𝐵))) → (fi‘(𝐴 ∪ 𝐵)) ⊆ (fi‘({ℝ*}
∪ (𝐴 ∪ 𝐵)))) |
35 | 32, 33, 34 | mp2an 704 |
. . 3
⊢
(fi‘(𝐴 ∪
𝐵)) ⊆
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) |
36 | | fvex 6113 |
. . . . 5
⊢
(topGen‘(fi‘(𝐴 ∪ 𝐵))) ∈ V |
37 | | ovex 6577 |
. . . . . . . . . 10
⊢
(0(,]+∞) ∈ V |
38 | | ovex 6577 |
. . . . . . . . . 10
⊢
(-∞[,)1) ∈ V |
39 | 37, 38 | unipr 4385 |
. . . . . . . . 9
⊢ ∪ {(0(,]+∞), (-∞[,)1)} = ((0(,]+∞) ∪
(-∞[,)1)) |
40 | | iocssxr 12128 |
. . . . . . . . . . 11
⊢
(0(,]+∞) ⊆ ℝ* |
41 | | icossxr 12129 |
. . . . . . . . . . 11
⊢
(-∞[,)1) ⊆ ℝ* |
42 | 40, 41 | unssi 3750 |
. . . . . . . . . 10
⊢
((0(,]+∞) ∪ (-∞[,)1)) ⊆
ℝ* |
43 | | mnfxr 9975 |
. . . . . . . . . . . . 13
⊢ -∞
∈ ℝ* |
44 | | 0xr 9965 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ* |
45 | | pnfxr 9971 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
46 | | mnflt0 11835 |
. . . . . . . . . . . . . 14
⊢ -∞
< 0 |
47 | | 0lepnf 11842 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
+∞ |
48 | | df-icc 12053 |
. . . . . . . . . . . . . . 15
⊢ [,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
49 | | df-ioc 12051 |
. . . . . . . . . . . . . . 15
⊢ (,] =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 ≤ 𝑦)}) |
50 | | xrltnle 9984 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (0 <
𝑤 ↔ ¬ 𝑤 ≤ 0)) |
51 | | xrletr 11865 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ*
∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑤 ≤ 0 ∧ 0
≤ +∞) → 𝑤
≤ +∞)) |
52 | | xrlttr 11849 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((-∞ < 0 ∧ 0 < 𝑤) → -∞ < 𝑤)) |
53 | | xrltle 11858 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-∞
< 𝑤 → -∞ ≤
𝑤)) |
54 | 53 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (-∞ < 𝑤 → -∞ ≤ 𝑤)) |
55 | 52, 54 | syld 46 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((-∞ < 0 ∧ 0 < 𝑤) → -∞ ≤ 𝑤)) |
56 | 48, 49, 50, 48, 51, 55 | ixxun 12062 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ ℝ* ∧ 0 ∈
ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞
< 0 ∧ 0 ≤ +∞)) → ((-∞[,]0) ∪ (0(,]+∞)) =
(-∞[,]+∞)) |
57 | 46, 47, 56 | mpanr12 717 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ ℝ* ∧ 0 ∈ ℝ*
∧ +∞ ∈ ℝ*) → ((-∞[,]0) ∪
(0(,]+∞)) = (-∞[,]+∞)) |
58 | 43, 44, 45, 57 | mp3an 1416 |
. . . . . . . . . . . 12
⊢
((-∞[,]0) ∪ (0(,]+∞)) =
(-∞[,]+∞) |
59 | | 1re 9918 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
60 | 59 | rexri 9976 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ* |
61 | | 0lt1 10429 |
. . . . . . . . . . . . . 14
⊢ 0 <
1 |
62 | | df-ico 12052 |
. . . . . . . . . . . . . . 15
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
63 | | xrlelttr 11863 |
. . . . . . . . . . . . . . 15
⊢ ((𝑤 ∈ ℝ*
∧ 0 ∈ ℝ* ∧ 1 ∈ ℝ*) →
((𝑤 ≤ 0 ∧ 0 < 1)
→ 𝑤 <
1)) |
64 | 62, 48, 63 | ixxss2 12065 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℝ* ∧ 0 < 1) → (-∞[,]0) ⊆
(-∞[,)1)) |
65 | 60, 61, 64 | mp2an 704 |
. . . . . . . . . . . . 13
⊢
(-∞[,]0) ⊆ (-∞[,)1) |
66 | | unss1 3744 |
. . . . . . . . . . . . 13
⊢
((-∞[,]0) ⊆ (-∞[,)1) → ((-∞[,]0) ∪
(0(,]+∞)) ⊆ ((-∞[,)1) ∪ (0(,]+∞))) |
67 | 65, 66 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
((-∞[,]0) ∪ (0(,]+∞)) ⊆ ((-∞[,)1) ∪
(0(,]+∞)) |
68 | 58, 67 | eqsstr3i 3599 |
. . . . . . . . . . 11
⊢
(-∞[,]+∞) ⊆ ((-∞[,)1) ∪
(0(,]+∞)) |
69 | | iccmax 12120 |
. . . . . . . . . . 11
⊢
(-∞[,]+∞) = ℝ* |
70 | | uncom 3719 |
. . . . . . . . . . 11
⊢
((-∞[,)1) ∪ (0(,]+∞)) = ((0(,]+∞) ∪
(-∞[,)1)) |
71 | 68, 69, 70 | 3sstr3i 3606 |
. . . . . . . . . 10
⊢
ℝ* ⊆ ((0(,]+∞) ∪
(-∞[,)1)) |
72 | 42, 71 | eqssi 3584 |
. . . . . . . . 9
⊢
((0(,]+∞) ∪ (-∞[,)1)) =
ℝ* |
73 | 39, 72 | eqtri 2632 |
. . . . . . . 8
⊢ ∪ {(0(,]+∞), (-∞[,)1)} =
ℝ* |
74 | | fvex 6113 |
. . . . . . . . 9
⊢
(fi‘(𝐴 ∪
𝐵)) ∈
V |
75 | | ssun1 3738 |
. . . . . . . . . . . 12
⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵) |
76 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(0(,]+∞) = (0(,]+∞) |
77 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 0 → (𝑥(,]+∞) =
(0(,]+∞)) |
78 | 77 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → ((0(,]+∞) =
(𝑥(,]+∞) ↔
(0(,]+∞) = (0(,]+∞))) |
79 | 78 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ (0(,]+∞) = (0(,]+∞)) →
∃𝑥 ∈
ℝ* (0(,]+∞) = (𝑥(,]+∞)) |
80 | 44, 76, 79 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢
∃𝑥 ∈
ℝ* (0(,]+∞) = (𝑥(,]+∞) |
81 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(,]+∞) ∈
V |
82 | 12, 81 | elrnmpti 5297 |
. . . . . . . . . . . . . 14
⊢
((0(,]+∞) ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) ↔
∃𝑥 ∈
ℝ* (0(,]+∞) = (𝑥(,]+∞)) |
83 | 80, 82 | mpbir 220 |
. . . . . . . . . . . . 13
⊢
(0(,]+∞) ∈ ran (𝑥 ∈ ℝ* ↦ (𝑥(,]+∞)) |
84 | 83, 3 | eleqtrri 2687 |
. . . . . . . . . . . 12
⊢
(0(,]+∞) ∈ 𝐴 |
85 | 75, 84 | sselii 3565 |
. . . . . . . . . . 11
⊢
(0(,]+∞) ∈ (𝐴 ∪ 𝐵) |
86 | | ssun2 3739 |
. . . . . . . . . . . 12
⊢ 𝐵 ⊆ (𝐴 ∪ 𝐵) |
87 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(-∞[,)1) = (-∞[,)1) |
88 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 1 → (-∞[,)𝑥) =
(-∞[,)1)) |
89 | 88 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 1 → ((-∞[,)1) =
(-∞[,)𝑥) ↔
(-∞[,)1) = (-∞[,)1))) |
90 | 89 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℝ* ∧ (-∞[,)1) = (-∞[,)1)) →
∃𝑥 ∈
ℝ* (-∞[,)1) = (-∞[,)𝑥)) |
91 | 60, 87, 90 | mp2an 704 |
. . . . . . . . . . . . . 14
⊢
∃𝑥 ∈
ℝ* (-∞[,)1) = (-∞[,)𝑥) |
92 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(-∞[,)𝑥)
∈ V |
93 | 21, 92 | elrnmpti 5297 |
. . . . . . . . . . . . . 14
⊢
((-∞[,)1) ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) ↔
∃𝑥 ∈
ℝ* (-∞[,)1) = (-∞[,)𝑥)) |
94 | 91, 93 | mpbir 220 |
. . . . . . . . . . . . 13
⊢
(-∞[,)1) ∈ ran (𝑥 ∈ ℝ* ↦
(-∞[,)𝑥)) |
95 | 94, 5 | eleqtrri 2687 |
. . . . . . . . . . . 12
⊢
(-∞[,)1) ∈ 𝐵 |
96 | 86, 95 | sselii 3565 |
. . . . . . . . . . 11
⊢
(-∞[,)1) ∈ (𝐴 ∪ 𝐵) |
97 | | prssi 4293 |
. . . . . . . . . . 11
⊢
(((0(,]+∞) ∈ (𝐴 ∪ 𝐵) ∧ (-∞[,)1) ∈ (𝐴 ∪ 𝐵)) → {(0(,]+∞), (-∞[,)1)}
⊆ (𝐴 ∪ 𝐵)) |
98 | 85, 96, 97 | mp2an 704 |
. . . . . . . . . 10
⊢
{(0(,]+∞), (-∞[,)1)} ⊆ (𝐴 ∪ 𝐵) |
99 | | ssfii 8208 |
. . . . . . . . . . 11
⊢ ((𝐴 ∪ 𝐵) ∈ V → (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵))) |
100 | 31, 99 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝐴 ∪ 𝐵) ⊆ (fi‘(𝐴 ∪ 𝐵)) |
101 | 98, 100 | sstri 3577 |
. . . . . . . . 9
⊢
{(0(,]+∞), (-∞[,)1)} ⊆ (fi‘(𝐴 ∪ 𝐵)) |
102 | | eltg3i 20576 |
. . . . . . . . 9
⊢
(((fi‘(𝐴 ∪
𝐵)) ∈ V ∧
{(0(,]+∞), (-∞[,)1)} ⊆ (fi‘(𝐴 ∪ 𝐵))) → ∪
{(0(,]+∞), (-∞[,)1)} ∈ (topGen‘(fi‘(𝐴 ∪ 𝐵)))) |
103 | 74, 101, 102 | mp2an 704 |
. . . . . . . 8
⊢ ∪ {(0(,]+∞), (-∞[,)1)} ∈
(topGen‘(fi‘(𝐴
∪ 𝐵))) |
104 | 73, 103 | eqeltrri 2685 |
. . . . . . 7
⊢
ℝ* ∈ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
105 | | snssi 4280 |
. . . . . . 7
⊢
(ℝ* ∈ (topGen‘(fi‘(𝐴 ∪ 𝐵))) → {ℝ*} ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) |
106 | 104, 105 | ax-mp 5 |
. . . . . 6
⊢
{ℝ*} ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
107 | | bastg 20581 |
. . . . . . . 8
⊢
((fi‘(𝐴 ∪
𝐵)) ∈ V →
(fi‘(𝐴 ∪ 𝐵)) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) |
108 | 74, 107 | ax-mp 5 |
. . . . . . 7
⊢
(fi‘(𝐴 ∪
𝐵)) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵))) |
109 | 100, 108 | sstri 3577 |
. . . . . 6
⊢ (𝐴 ∪ 𝐵) ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
110 | 106, 109 | unssi 3750 |
. . . . 5
⊢
({ℝ*} ∪ (𝐴 ∪ 𝐵)) ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
111 | | fiss 8213 |
. . . . 5
⊢
(((topGen‘(fi‘(𝐴 ∪ 𝐵))) ∈ V ∧ ({ℝ*}
∪ (𝐴 ∪ 𝐵)) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) →
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ⊆
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵))))) |
112 | 36, 110, 111 | mp2an 704 |
. . . 4
⊢
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ⊆
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵)))) |
113 | | fibas 20592 |
. . . . 5
⊢
(fi‘(𝐴 ∪
𝐵)) ∈
TopBases |
114 | | tgcl 20584 |
. . . . 5
⊢
((fi‘(𝐴 ∪
𝐵)) ∈ TopBases →
(topGen‘(fi‘(𝐴
∪ 𝐵))) ∈
Top) |
115 | | fitop 20530 |
. . . . 5
⊢
((topGen‘(fi‘(𝐴 ∪ 𝐵))) ∈ Top →
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵)))) = (topGen‘(fi‘(𝐴 ∪ 𝐵)))) |
116 | 113, 114,
115 | mp2b 10 |
. . . 4
⊢
(fi‘(topGen‘(fi‘(𝐴 ∪ 𝐵)))) = (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
117 | 112, 116 | sseqtri 3600 |
. . 3
⊢
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ⊆ (topGen‘(fi‘(𝐴 ∪ 𝐵))) |
118 | | 2basgen 20605 |
. . 3
⊢
(((fi‘(𝐴 ∪
𝐵)) ⊆
(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))) ∧ (fi‘({ℝ*}
∪ (𝐴 ∪ 𝐵))) ⊆
(topGen‘(fi‘(𝐴
∪ 𝐵)))) →
(topGen‘(fi‘(𝐴
∪ 𝐵))) =
(topGen‘(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵))))) |
119 | 35, 117, 118 | mp2an 704 |
. 2
⊢
(topGen‘(fi‘(𝐴 ∪ 𝐵))) =
(topGen‘(fi‘({ℝ*} ∪ (𝐴 ∪ 𝐵)))) |
120 | 8, 119 | eqtr4i 2635 |
1
⊢
(ordTop‘ ≤ ) = (topGen‘(fi‘(𝐴 ∪ 𝐵))) |