Proof of Theorem tuslem
Step | Hyp | Ref
| Expression |
1 | | baseid 16531 |
. . . 4
⊢ Base =
Slot (Base‘ndx) |
2 | | 1re 10629 |
. . . . . 6
⊢ 1 ∈
ℝ |
3 | | 1lt9 11831 |
. . . . . 6
⊢ 1 <
9 |
4 | 2, 3 | ltneii 10741 |
. . . . 5
⊢ 1 ≠
9 |
5 | | basendx 16535 |
. . . . . 6
⊢
(Base‘ndx) = 1 |
6 | | tsetndx 16647 |
. . . . . 6
⊢
(TopSet‘ndx) = 9 |
7 | 5, 6 | neeq12i 3079 |
. . . . 5
⊢
((Base‘ndx) ≠ (TopSet‘ndx) ↔ 1 ≠
9) |
8 | 4, 7 | mpbir 232 |
. . . 4
⊢
(Base‘ndx) ≠ (TopSet‘ndx) |
9 | 1, 8 | setsnid 16527 |
. . 3
⊢
(Base‘{〈(Base‘ndx), dom ∪
𝑈〉,
〈(UnifSet‘ndx), 𝑈〉}) =
(Base‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉)) |
10 | | ustbas2 22761 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈) |
11 | | uniexg 7456 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈
∈ V) |
12 | | dmexg 7602 |
. . . . 5
⊢ (∪ 𝑈
∈ V → dom ∪ 𝑈 ∈ V) |
13 | | eqid 2818 |
. . . . . 6
⊢
{〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} = {〈(Base‘ndx), dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉} |
14 | | df-unif 16576 |
. . . . . 6
⊢ UnifSet =
Slot ;13 |
15 | | 1nn 11637 |
. . . . . . 7
⊢ 1 ∈
ℕ |
16 | | 3nn0 11903 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
17 | | 1nn0 11901 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
18 | | 1lt10 12225 |
. . . . . . 7
⊢ 1 <
;10 |
19 | 15, 16, 17, 18 | declti 12124 |
. . . . . 6
⊢ 1 <
;13 |
20 | | 3nn 11704 |
. . . . . . 7
⊢ 3 ∈
ℕ |
21 | 17, 20 | decnncl 12106 |
. . . . . 6
⊢ ;13 ∈ ℕ |
22 | 13, 14, 19, 21 | 2strbas 16591 |
. . . . 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 2853 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘{〈(Base‘ndx), dom
∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉})) |
25 | | tuslem.k |
. . . . 5
⊢ 𝐾 = (toUnifSp‘𝑈) |
26 | | tusval 22802 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({〈(Base‘ndx),
dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑈)〉)) |
27 | 25, 26 | syl5eq 2865 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 = ({〈(Base‘ndx), dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑈)〉)) |
28 | 27 | fveq2d 6667 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (Base‘𝐾) =
(Base‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
29 | 9, 24, 28 | 3eqtr4a 2879 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) |
30 | | unifid 16666 |
. . . 4
⊢ UnifSet =
Slot (UnifSet‘ndx) |
31 | | 9re 11724 |
. . . . . 6
⊢ 9 ∈
ℝ |
32 | | 9nn0 11909 |
. . . . . . 7
⊢ 9 ∈
ℕ0 |
33 | | 9lt10 12217 |
. . . . . . 7
⊢ 9 <
;10 |
34 | 15, 16, 32, 33 | declti 12124 |
. . . . . 6
⊢ 9 <
;13 |
35 | 31, 34 | gtneii 10740 |
. . . . 5
⊢ ;13 ≠ 9 |
36 | | unifndx 16665 |
. . . . . 6
⊢
(UnifSet‘ndx) = ;13 |
37 | 36, 6 | neeq12i 3079 |
. . . . 5
⊢
((UnifSet‘ndx) ≠ (TopSet‘ndx) ↔ ;13 ≠ 9) |
38 | 35, 37 | mpbir 232 |
. . . 4
⊢
(UnifSet‘ndx) ≠ (TopSet‘ndx) |
39 | 30, 38 | setsnid 16527 |
. . 3
⊢
(UnifSet‘{〈(Base‘ndx), dom ∪
𝑈〉,
〈(UnifSet‘ndx), 𝑈〉}) =
(UnifSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉)) |
40 | 13, 14, 19, 21 | 2strop 16592 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘{〈(Base‘ndx),
dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉})) |
41 | 27 | fveq2d 6667 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (UnifSet‘𝐾) =
(UnifSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
42 | 39, 40, 41 | 3eqtr4a 2879 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) |
43 | 27 | fveq2d 6667 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) =
(TopSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
44 | | prex 5323 |
. . . . 5
⊢
{〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} ∈ V |
45 | | fvex 6676 |
. . . . 5
⊢
(unifTop‘𝑈)
∈ V |
46 | | tsetid 16648 |
. . . . . 6
⊢ TopSet =
Slot (TopSet‘ndx) |
47 | 46 | setsid 16526 |
. . . . 5
⊢
(({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} ∈ V ∧ (unifTop‘𝑈) ∈ V) →
(unifTop‘𝑈) =
(TopSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
48 | 44, 45, 47 | mp2an 688 |
. . . 4
⊢
(unifTop‘𝑈) =
(TopSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉)) |
49 | 43, 48 | syl6reqr 2872 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopSet‘𝐾)) |
50 | | utopbas 22771 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |
51 | 49 | unieqd 4840 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = ∪
(TopSet‘𝐾)) |
52 | 50, 29, 51 | 3eqtr3rd 2862 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (TopSet‘𝐾) = (Base‘𝐾)) |
53 | 52 | oveq2d 7161 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = ((TopSet‘𝐾) ↾t (Base‘𝐾))) |
54 | | fvex 6676 |
. . . . 5
⊢
(TopSet‘𝐾)
∈ V |
55 | | eqid 2818 |
. . . . . 6
⊢ ∪ (TopSet‘𝐾) = ∪
(TopSet‘𝐾) |
56 | 55 | restid 16695 |
. . . . 5
⊢
((TopSet‘𝐾)
∈ V → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾)) |
57 | 54, 56 | ax-mp 5 |
. . . 4
⊢
((TopSet‘𝐾)
↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾) |
58 | | eqid 2818 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
59 | | eqid 2818 |
. . . . 5
⊢
(TopSet‘𝐾) =
(TopSet‘𝐾) |
60 | 58, 59 | topnval 16696 |
. . . 4
⊢
((TopSet‘𝐾)
↾t (Base‘𝐾)) = (TopOpen‘𝐾) |
61 | 53, 57, 60 | 3eqtr3g 2876 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopOpen‘𝐾)) |
62 | 49, 61 | eqtrd 2853 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopOpen‘𝐾)) |
63 | 29, 42, 62 | 3jca 1120 |
1
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) |