Step | Hyp | Ref
| Expression |
1 | | baseid 17091 |
. . . 4
⊢ Base =
Slot (Base‘ndx) |
2 | | 1re 11160 |
. . . . . 6
⊢ 1 ∈
ℝ |
3 | | 1lt9 12364 |
. . . . . 6
⊢ 1 <
9 |
4 | 2, 3 | ltneii 11273 |
. . . . 5
⊢ 1 ≠
9 |
5 | | basendx 17097 |
. . . . . 6
⊢
(Base‘ndx) = 1 |
6 | | tsetndx 17238 |
. . . . . 6
⊢
(TopSet‘ndx) = 9 |
7 | 5, 6 | neeq12i 3007 |
. . . . 5
⊢
((Base‘ndx) ≠ (TopSet‘ndx) ↔ 1 ≠
9) |
8 | 4, 7 | mpbir 230 |
. . . 4
⊢
(Base‘ndx) ≠ (TopSet‘ndx) |
9 | 1, 8 | setsnid 17086 |
. . 3
⊢
(Base‘{⟨(Base‘ndx), dom ∪
𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩}) =
(Base‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩)) |
10 | | ustbas2 23593 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈) |
11 | | uniexg 7678 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈
∈ V) |
12 | | dmexg 7841 |
. . . . 5
⊢ (∪ 𝑈
∈ V → dom ∪ 𝑈 ∈ V) |
13 | | eqid 2733 |
. . . . . 6
⊢
{⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} = {⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} |
14 | | df-unif 17161 |
. . . . . 6
⊢ UnifSet =
Slot ;13 |
15 | | 1nn 12169 |
. . . . . . 7
⊢ 1 ∈
ℕ |
16 | | 3nn0 12436 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
17 | | 1nn0 12434 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
18 | | 1lt10 12762 |
. . . . . . 7
⊢ 1 <
;10 |
19 | 15, 16, 17, 18 | declti 12661 |
. . . . . 6
⊢ 1 <
;13 |
20 | | 3nn 12237 |
. . . . . . 7
⊢ 3 ∈
ℕ |
21 | 17, 20 | decnncl 12643 |
. . . . . 6
⊢ ;13 ∈ ℕ |
22 | 13, 14, 19, 21 | 2strbas 17111 |
. . . . 5
⊢ (dom
∪ 𝑈 ∈ V → dom ∪ 𝑈 =
(Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩})) |
23 | 11, 12, 22 | 3syl 18 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → dom ∪ 𝑈 =
(Base‘{⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩})) |
24 | 10, 23 | eqtrd 2773 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘{⟨(Base‘ndx), dom
∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩})) |
25 | | tuslem.k |
. . . . 5
⊢ 𝐾 = (toUnifSp‘𝑈) |
26 | | tusval 23633 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({⟨(Base‘ndx),
dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet
⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)) |
27 | 25, 26 | eqtrid 2785 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 = ({⟨(Base‘ndx), dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩} sSet
⟨(TopSet‘ndx), (unifTop‘𝑈)⟩)) |
28 | 27 | fveq2d 6847 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (Base‘𝐾) =
(Base‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩))) |
29 | 9, 24, 28 | 3eqtr4a 2799 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) |
30 | | unifid 17282 |
. . . 4
⊢ UnifSet =
Slot (UnifSet‘ndx) |
31 | | 9re 12257 |
. . . . . 6
⊢ 9 ∈
ℝ |
32 | | 9nn0 12442 |
. . . . . . 7
⊢ 9 ∈
ℕ0 |
33 | | 9lt10 12754 |
. . . . . . 7
⊢ 9 <
;10 |
34 | 15, 16, 32, 33 | declti 12661 |
. . . . . 6
⊢ 9 <
;13 |
35 | 31, 34 | gtneii 11272 |
. . . . 5
⊢ ;13 ≠ 9 |
36 | | unifndx 17281 |
. . . . . 6
⊢
(UnifSet‘ndx) = ;13 |
37 | 36, 6 | neeq12i 3007 |
. . . . 5
⊢
((UnifSet‘ndx) ≠ (TopSet‘ndx) ↔ ;13 ≠ 9) |
38 | 35, 37 | mpbir 230 |
. . . 4
⊢
(UnifSet‘ndx) ≠ (TopSet‘ndx) |
39 | 30, 38 | setsnid 17086 |
. . 3
⊢
(UnifSet‘{⟨(Base‘ndx), dom ∪
𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩}) =
(UnifSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩)) |
40 | 13, 14, 19, 21 | 2strop 17112 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘{⟨(Base‘ndx),
dom ∪ 𝑈⟩, ⟨(UnifSet‘ndx), 𝑈⟩})) |
41 | 27 | fveq2d 6847 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (UnifSet‘𝐾) =
(UnifSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩))) |
42 | 39, 40, 41 | 3eqtr4a 2799 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) |
43 | | prex 5390 |
. . . . 5
⊢
{⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} ∈ V |
44 | | fvex 6856 |
. . . . 5
⊢
(unifTop‘𝑈)
∈ V |
45 | | tsetid 17239 |
. . . . . 6
⊢ TopSet =
Slot (TopSet‘ndx) |
46 | 45 | setsid 17085 |
. . . . 5
⊢
(({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} ∈ V ∧ (unifTop‘𝑈) ∈ V) →
(unifTop‘𝑈) =
(TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩))) |
47 | 43, 44, 46 | mp2an 691 |
. . . 4
⊢
(unifTop‘𝑈) =
(TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩)) |
48 | 27 | fveq2d 6847 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) =
(TopSet‘({⟨(Base‘ndx), dom ∪ 𝑈⟩,
⟨(UnifSet‘ndx), 𝑈⟩} sSet ⟨(TopSet‘ndx),
(unifTop‘𝑈)⟩))) |
49 | 47, 48 | eqtr4id 2792 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopSet‘𝐾)) |
50 | | utopbas 23603 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |
51 | 49 | unieqd 4880 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = ∪
(TopSet‘𝐾)) |
52 | 50, 29, 51 | 3eqtr3rd 2782 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (TopSet‘𝐾) = (Base‘𝐾)) |
53 | 52 | oveq2d 7374 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = ((TopSet‘𝐾) ↾t (Base‘𝐾))) |
54 | | fvex 6856 |
. . . . 5
⊢
(TopSet‘𝐾)
∈ V |
55 | | eqid 2733 |
. . . . . 6
⊢ ∪ (TopSet‘𝐾) = ∪
(TopSet‘𝐾) |
56 | 55 | restid 17320 |
. . . . 5
⊢
((TopSet‘𝐾)
∈ V → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾)) |
57 | 54, 56 | ax-mp 5 |
. . . 4
⊢
((TopSet‘𝐾)
↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾) |
58 | | eqid 2733 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
59 | | eqid 2733 |
. . . . 5
⊢
(TopSet‘𝐾) =
(TopSet‘𝐾) |
60 | 58, 59 | topnval 17321 |
. . . 4
⊢
((TopSet‘𝐾)
↾t (Base‘𝐾)) = (TopOpen‘𝐾) |
61 | 53, 57, 60 | 3eqtr3g 2796 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopOpen‘𝐾)) |
62 | 49, 61 | eqtrd 2773 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopOpen‘𝐾)) |
63 | 29, 42, 62 | 3jca 1129 |
1
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) |