Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) |
2 | | eqid 2610 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) |
3 | 1, 2 | leordtval2 20826 |
. . 3
⊢
(ordTop‘ ≤ ) = (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦))))) |
4 | | fvex 6113 |
. . . 4
⊢
(fi‘ran 𝐹)
∈ V |
5 | | fvex 6113 |
. . . . . 6
⊢
(ordTop‘ ≤ ) ∈ V |
6 | | lecldbas.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑥 ∈ ran [,] ↦ (ℝ*
∖ 𝑥)) |
7 | | iccf 12143 |
. . . . . . . . . . 11
⊢
[,]:(ℝ* × ℝ*)⟶𝒫
ℝ* |
8 | | ffn 5958 |
. . . . . . . . . . 11
⊢
([,]:(ℝ* × ℝ*)⟶𝒫
ℝ* → [,] Fn (ℝ* ×
ℝ*)) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ [,] Fn
(ℝ* × ℝ*) |
10 | | ovelrn 6708 |
. . . . . . . . . 10
⊢ ([,] Fn
(ℝ* × ℝ*) → (𝑥 ∈ ran [,] ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑥 =
(𝑎[,]𝑏))) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ ran [,] ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏)) |
12 | | difeq2 3684 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑎[,]𝑏) → (ℝ* ∖ 𝑥) = (ℝ* ∖
(𝑎[,]𝑏))) |
13 | | iccordt 20828 |
. . . . . . . . . . . . 13
⊢ (𝑎[,]𝑏) ∈ (Clsd‘(ordTop‘ ≤
)) |
14 | | letopuni 20821 |
. . . . . . . . . . . . . 14
⊢
ℝ* = ∪ (ordTop‘ ≤
) |
15 | 14 | cldopn 20645 |
. . . . . . . . . . . . 13
⊢ ((𝑎[,]𝑏) ∈ (Clsd‘(ordTop‘ ≤ ))
→ (ℝ* ∖ (𝑎[,]𝑏)) ∈ (ordTop‘ ≤
)) |
16 | 13, 15 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
(ℝ* ∖ (𝑎[,]𝑏)) ∈ (ordTop‘ ≤
) |
17 | 12, 16 | syl6eqel 2696 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑎[,]𝑏) → (ℝ* ∖ 𝑥) ∈ (ordTop‘ ≤
)) |
18 | 17 | rexlimivw 3011 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
ℝ* 𝑥 =
(𝑎[,]𝑏) → (ℝ* ∖ 𝑥) ∈ (ordTop‘ ≤
)) |
19 | 18 | rexlimivw 3011 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑥 = (𝑎[,]𝑏) → (ℝ* ∖ 𝑥) ∈ (ordTop‘ ≤
)) |
20 | 11, 19 | sylbi 206 |
. . . . . . . 8
⊢ (𝑥 ∈ ran [,] →
(ℝ* ∖ 𝑥) ∈ (ordTop‘ ≤
)) |
21 | 6, 20 | fmpti 6291 |
. . . . . . 7
⊢ 𝐹:ran [,]⟶(ordTop‘
≤ ) |
22 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:ran [,]⟶(ordTop‘
≤ ) → ran 𝐹 ⊆
(ordTop‘ ≤ )) |
23 | 21, 22 | ax-mp 5 |
. . . . . 6
⊢ ran 𝐹 ⊆ (ordTop‘ ≤
) |
24 | 5, 23 | ssexi 4731 |
. . . . 5
⊢ ran 𝐹 ∈ V |
25 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)) =
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) |
26 | | mnfxr 9975 |
. . . . . . . . . . 11
⊢ -∞
∈ ℝ* |
27 | | fnovrn 6707 |
. . . . . . . . . . 11
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ -∞ ∈
ℝ* ∧ 𝑦
∈ ℝ*) → (-∞[,]𝑦) ∈ ran [,]) |
28 | 9, 26, 27 | mp3an12 1406 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ (-∞[,]𝑦)
∈ ran [,]) |
29 | 26 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ -∞ ∈ ℝ*) |
30 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ∈
ℝ*) |
31 | | pnfxr 9971 |
. . . . . . . . . . . . . . 15
⊢ +∞
∈ ℝ* |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ +∞ ∈ ℝ*) |
33 | | mnfle 11845 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ -∞ ≤ 𝑦) |
34 | | pnfge 11840 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
35 | | df-icc 12053 |
. . . . . . . . . . . . . . 15
⊢ [,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 ≤ 𝑏)}) |
36 | | df-ioc 12051 |
. . . . . . . . . . . . . . 15
⊢ (,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)}) |
37 | | xrltnle 9984 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ 𝑧 ∈
ℝ*) → (𝑦 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑦)) |
38 | | xrletr 11865 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 ≤ 𝑦 ∧ 𝑦 ≤ +∞) → 𝑧 ≤ +∞)) |
39 | | xrlelttr 11863 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ ((-∞ ≤ 𝑦
∧ 𝑦 < 𝑧) → -∞ < 𝑧)) |
40 | | xrltle 11858 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 𝑧 ∈ ℝ*) → (-∞
< 𝑧 → -∞ ≤
𝑧)) |
41 | 40 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ (-∞ < 𝑧
→ -∞ ≤ 𝑧)) |
42 | 39, 41 | syld 46 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ ((-∞ ≤ 𝑦
∧ 𝑦 < 𝑧) → -∞ ≤ 𝑧)) |
43 | 35, 36, 37, 35, 38, 42 | ixxun 12062 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ ≤ 𝑦 ∧ 𝑦 ≤ +∞)) → ((-∞[,]𝑦) ∪ (𝑦(,]+∞)) =
(-∞[,]+∞)) |
44 | 29, 30, 32, 33, 34, 43 | syl32anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ((-∞[,]𝑦)
∪ (𝑦(,]+∞)) =
(-∞[,]+∞)) |
45 | | iccmax 12120 |
. . . . . . . . . . . . 13
⊢
(-∞[,]+∞) = ℝ* |
46 | 44, 45 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ ((-∞[,]𝑦)
∪ (𝑦(,]+∞)) =
ℝ*) |
47 | | iccssxr 12127 |
. . . . . . . . . . . . 13
⊢
(-∞[,]𝑦)
⊆ ℝ* |
48 | 35, 36, 37 | ixxdisj 12061 |
. . . . . . . . . . . . . 14
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅) |
49 | 26, 31, 48 | mp3an13 1407 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ((-∞[,]𝑦)
∩ (𝑦(,]+∞)) =
∅) |
50 | | uneqdifeq 4009 |
. . . . . . . . . . . . 13
⊢
(((-∞[,]𝑦)
⊆ ℝ* ∧ ((-∞[,]𝑦) ∩ (𝑦(,]+∞)) = ∅) →
(((-∞[,]𝑦) ∪
(𝑦(,]+∞)) =
ℝ* ↔ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞))) |
51 | 47, 49, 50 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (((-∞[,]𝑦)
∪ (𝑦(,]+∞)) =
ℝ* ↔ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞))) |
52 | 46, 51 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (ℝ* ∖ (-∞[,]𝑦)) = (𝑦(,]+∞)) |
53 | 52 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ (𝑦(,]+∞) =
(ℝ* ∖ (-∞[,]𝑦))) |
54 | | difeq2 3684 |
. . . . . . . . . . . 12
⊢ (𝑥 = (-∞[,]𝑦) → (ℝ*
∖ 𝑥) =
(ℝ* ∖ (-∞[,]𝑦))) |
55 | 54 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑥 = (-∞[,]𝑦) → ((𝑦(,]+∞) = (ℝ* ∖
𝑥) ↔ (𝑦(,]+∞) =
(ℝ* ∖ (-∞[,]𝑦)))) |
56 | 55 | rspcev 3282 |
. . . . . . . . . 10
⊢
(((-∞[,]𝑦)
∈ ran [,] ∧ (𝑦(,]+∞) = (ℝ* ∖
(-∞[,]𝑦))) →
∃𝑥 ∈ ran
[,](𝑦(,]+∞) =
(ℝ* ∖ 𝑥)) |
57 | 28, 53, 56 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ ∃𝑥 ∈ ran
[,](𝑦(,]+∞) =
(ℝ* ∖ 𝑥)) |
58 | | xrex 11705 |
. . . . . . . . . . 11
⊢
ℝ* ∈ V |
59 | | difexg 4735 |
. . . . . . . . . . 11
⊢
(ℝ* ∈ V → (ℝ* ∖ 𝑥) ∈ V) |
60 | 58, 59 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℝ* ∖ 𝑥) ∈ V |
61 | 6, 60 | elrnmpti 5297 |
. . . . . . . . 9
⊢ ((𝑦(,]+∞) ∈ ran 𝐹 ↔ ∃𝑥 ∈ ran [,](𝑦(,]+∞) =
(ℝ* ∖ 𝑥)) |
62 | 57, 61 | sylibr 223 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ (𝑦(,]+∞)
∈ ran 𝐹) |
63 | 25, 62 | fmpti 6291 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)):ℝ*⟶ran
𝐹 |
64 | | frn 5966 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)):ℝ*⟶ran
𝐹 → ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
⊆ ran 𝐹) |
65 | 63, 64 | ax-mp 5 |
. . . . . 6
⊢ ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ⊆ ran 𝐹 |
66 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)) =
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) |
67 | | fnovrn 6707 |
. . . . . . . . . . 11
⊢ (([,] Fn
(ℝ* × ℝ*) ∧ 𝑦 ∈ ℝ* ∧ +∞
∈ ℝ*) → (𝑦[,]+∞) ∈ ran [,]) |
68 | 9, 31, 67 | mp3an13 1407 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ (𝑦[,]+∞)
∈ ran [,]) |
69 | | df-ico 12052 |
. . . . . . . . . . . . . . 15
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) |
70 | | xrlenlt 9982 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ 𝑧 ∈
ℝ*) → (𝑦 ≤ 𝑧 ↔ ¬ 𝑧 < 𝑦)) |
71 | | xrltletr 11864 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 < 𝑦 ∧ 𝑦 ≤ +∞) → 𝑧 < +∞)) |
72 | | xrltle 11858 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑧 < +∞ → 𝑧 ≤ +∞)) |
73 | 72 | 3adant2 1073 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ +∞ ∈ ℝ*) → (𝑧 < +∞ → 𝑧 ≤
+∞)) |
74 | 71, 73 | syld 46 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℝ*
∧ 𝑦 ∈
ℝ* ∧ +∞ ∈ ℝ*) → ((𝑧 < 𝑦 ∧ 𝑦 ≤ +∞) → 𝑧 ≤ +∞)) |
75 | | xrletr 11865 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ 𝑧 ∈ ℝ*)
→ ((-∞ ≤ 𝑦
∧ 𝑦 ≤ 𝑧) → -∞ ≤ 𝑧)) |
76 | 69, 35, 70, 35, 74, 75 | ixxun 12062 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ ≤ 𝑦 ∧ 𝑦 ≤ +∞)) → ((-∞[,)𝑦) ∪ (𝑦[,]+∞)) =
(-∞[,]+∞)) |
77 | 29, 30, 32, 33, 34, 76 | syl32anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ((-∞[,)𝑦)
∪ (𝑦[,]+∞)) =
(-∞[,]+∞)) |
78 | | uncom 3719 |
. . . . . . . . . . . . 13
⊢
((-∞[,)𝑦)
∪ (𝑦[,]+∞)) =
((𝑦[,]+∞) ∪
(-∞[,)𝑦)) |
79 | 77, 78, 45 | 3eqtr3g 2667 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ ((𝑦[,]+∞)
∪ (-∞[,)𝑦)) =
ℝ*) |
80 | | iccssxr 12127 |
. . . . . . . . . . . . 13
⊢ (𝑦[,]+∞) ⊆
ℝ* |
81 | | incom 3767 |
. . . . . . . . . . . . . 14
⊢ ((𝑦[,]+∞) ∩
(-∞[,)𝑦)) =
((-∞[,)𝑦) ∩
(𝑦[,]+∞)) |
82 | 69, 35, 70 | ixxdisj 12061 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ* ∧ +∞
∈ ℝ*) → ((-∞[,)𝑦) ∩ (𝑦[,]+∞)) = ∅) |
83 | 26, 31, 82 | mp3an13 1407 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ((-∞[,)𝑦)
∩ (𝑦[,]+∞)) =
∅) |
84 | 81, 83 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ((𝑦[,]+∞)
∩ (-∞[,)𝑦)) =
∅) |
85 | | uneqdifeq 4009 |
. . . . . . . . . . . . 13
⊢ (((𝑦[,]+∞) ⊆
ℝ* ∧ ((𝑦[,]+∞) ∩ (-∞[,)𝑦)) = ∅) → (((𝑦[,]+∞) ∪
(-∞[,)𝑦)) =
ℝ* ↔ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦))) |
86 | 80, 84, 85 | sylancr 694 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (((𝑦[,]+∞)
∪ (-∞[,)𝑦)) =
ℝ* ↔ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦))) |
87 | 79, 86 | mpbid 221 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
→ (ℝ* ∖ (𝑦[,]+∞)) = (-∞[,)𝑦)) |
88 | 87 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑦 ∈ ℝ*
→ (-∞[,)𝑦) =
(ℝ* ∖ (𝑦[,]+∞))) |
89 | | difeq2 3684 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦[,]+∞) → (ℝ*
∖ 𝑥) =
(ℝ* ∖ (𝑦[,]+∞))) |
90 | 89 | eqeq2d 2620 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦[,]+∞) → ((-∞[,)𝑦) = (ℝ* ∖
𝑥) ↔ (-∞[,)𝑦) = (ℝ* ∖
(𝑦[,]+∞)))) |
91 | 90 | rspcev 3282 |
. . . . . . . . . 10
⊢ (((𝑦[,]+∞) ∈ ran [,]
∧ (-∞[,)𝑦) =
(ℝ* ∖ (𝑦[,]+∞))) → ∃𝑥 ∈ ran [,](-∞[,)𝑦) = (ℝ* ∖
𝑥)) |
92 | 68, 88, 91 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ*
→ ∃𝑥 ∈ ran
[,](-∞[,)𝑦) =
(ℝ* ∖ 𝑥)) |
93 | 6, 60 | elrnmpti 5297 |
. . . . . . . . 9
⊢
((-∞[,)𝑦)
∈ ran 𝐹 ↔
∃𝑥 ∈ ran
[,](-∞[,)𝑦) =
(ℝ* ∖ 𝑥)) |
94 | 92, 93 | sylibr 223 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ*
→ (-∞[,)𝑦)
∈ ran 𝐹) |
95 | 66, 94 | fmpti 6291 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)):ℝ*⟶ran 𝐹 |
96 | | frn 5966 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)):ℝ*⟶ran 𝐹 → ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ⊆ ran
𝐹) |
97 | 95, 96 | ax-mp 5 |
. . . . . 6
⊢ ran
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) ⊆ ran 𝐹 |
98 | 65, 97 | unssi 3750 |
. . . . 5
⊢ (ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ⊆
ran 𝐹 |
99 | | fiss 8213 |
. . . . 5
⊢ ((ran
𝐹 ∈ V ∧ (ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ⊆
ran 𝐹) →
(fi‘(ran (𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)))) ⊆
(fi‘ran 𝐹)) |
100 | 24, 98, 99 | mp2an 704 |
. . . 4
⊢
(fi‘(ran (𝑦
∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)))) ⊆
(fi‘ran 𝐹) |
101 | | tgss 20583 |
. . . 4
⊢
(((fi‘ran 𝐹)
∈ V ∧ (fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦))))
⊆ (fi‘ran 𝐹))
→ (topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))))
⊆ (topGen‘(fi‘ran 𝐹))) |
102 | 4, 100, 101 | mp2an 704 |
. . 3
⊢
(topGen‘(fi‘(ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))))
⊆ (topGen‘(fi‘ran 𝐹)) |
103 | 3, 102 | eqsstri 3598 |
. 2
⊢
(ordTop‘ ≤ ) ⊆ (topGen‘(fi‘ran 𝐹)) |
104 | | letop 20820 |
. . 3
⊢
(ordTop‘ ≤ ) ∈ Top |
105 | | tgfiss 20606 |
. . 3
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ ran 𝐹 ⊆ (ordTop‘ ≤ )) →
(topGen‘(fi‘ran 𝐹)) ⊆ (ordTop‘ ≤
)) |
106 | 104, 23, 105 | mp2an 704 |
. 2
⊢
(topGen‘(fi‘ran 𝐹)) ⊆ (ordTop‘ ≤
) |
107 | 103, 106 | eqssi 3584 |
1
⊢
(ordTop‘ ≤ ) = (topGen‘(fi‘ran 𝐹)) |