Proof of Theorem tuslem
| Step | Hyp | Ref
| Expression |
| 1 | | baseid 17250 |
. . . 4
⊢ Base =
Slot (Base‘ndx) |
| 2 | | tsetndxnbasendx 17400 |
. . . . 5
⊢
(TopSet‘ndx) ≠ (Base‘ndx) |
| 3 | 2 | necomi 2995 |
. . . 4
⊢
(Base‘ndx) ≠ (TopSet‘ndx) |
| 4 | 1, 3 | setsnid 17245 |
. . 3
⊢
(Base‘{〈(Base‘ndx), dom ∪
𝑈〉,
〈(UnifSet‘ndx), 𝑈〉}) =
(Base‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉)) |
| 5 | | ustbas2 24234 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = dom ∪ 𝑈) |
| 6 | | uniexg 7760 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ 𝑈
∈ V) |
| 7 | | dmexg 7923 |
. . . . 5
⊢ (∪ 𝑈
∈ V → dom ∪ 𝑈 ∈ V) |
| 8 | | eqid 2737 |
. . . . . 6
⊢
{〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} = {〈(Base‘ndx), dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉} |
| 9 | | basendxltunifndx 17442 |
. . . . . 6
⊢
(Base‘ndx) < (UnifSet‘ndx) |
| 10 | | unifndxnn 17441 |
. . . . . 6
⊢
(UnifSet‘ndx) ∈ ℕ |
| 11 | 8, 9, 10 | 2strbas1 17272 |
. . . . 5
⊢ (dom
∪ 𝑈 ∈ V → dom ∪ 𝑈 =
(Base‘{〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉})) |
| 12 | 6, 7, 11 | 3syl 18 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → dom ∪ 𝑈 =
(Base‘{〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉})) |
| 13 | 5, 12 | eqtrd 2777 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘{〈(Base‘ndx), dom
∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉})) |
| 14 | | tuslem.k |
. . . . 5
⊢ 𝐾 = (toUnifSp‘𝑈) |
| 15 | | tusval 24274 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (toUnifSp‘𝑈) = ({〈(Base‘ndx),
dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑈)〉)) |
| 16 | 14, 15 | eqtrid 2789 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝐾 = ({〈(Base‘ndx), dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉} sSet
〈(TopSet‘ndx), (unifTop‘𝑈)〉)) |
| 17 | 16 | fveq2d 6910 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (Base‘𝐾) =
(Base‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
| 18 | 4, 13, 17 | 3eqtr4a 2803 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = (Base‘𝐾)) |
| 19 | | unifid 17440 |
. . . 4
⊢ UnifSet =
Slot (UnifSet‘ndx) |
| 20 | | unifndxntsetndx 17444 |
. . . 4
⊢
(UnifSet‘ndx) ≠ (TopSet‘ndx) |
| 21 | 19, 20 | setsnid 17245 |
. . 3
⊢
(UnifSet‘{〈(Base‘ndx), dom ∪
𝑈〉,
〈(UnifSet‘ndx), 𝑈〉}) =
(UnifSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉)) |
| 22 | 8, 9, 10, 19 | 2strop1 17273 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘{〈(Base‘ndx),
dom ∪ 𝑈〉, 〈(UnifSet‘ndx), 𝑈〉})) |
| 23 | 16 | fveq2d 6910 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (UnifSet‘𝐾) =
(UnifSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
| 24 | 21, 22, 23 | 3eqtr4a 2803 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑈 = (UnifSet‘𝐾)) |
| 25 | | prex 5437 |
. . . . 5
⊢
{〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} ∈ V |
| 26 | | fvex 6919 |
. . . . 5
⊢
(unifTop‘𝑈)
∈ V |
| 27 | | tsetid 17397 |
. . . . . 6
⊢ TopSet =
Slot (TopSet‘ndx) |
| 28 | 27 | setsid 17244 |
. . . . 5
⊢
(({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} ∈ V ∧ (unifTop‘𝑈) ∈ V) →
(unifTop‘𝑈) =
(TopSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
| 29 | 25, 26, 28 | mp2an 692 |
. . . 4
⊢
(unifTop‘𝑈) =
(TopSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉)) |
| 30 | 16 | fveq2d 6910 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) =
(TopSet‘({〈(Base‘ndx), dom ∪ 𝑈〉,
〈(UnifSet‘ndx), 𝑈〉} sSet 〈(TopSet‘ndx),
(unifTop‘𝑈)〉))) |
| 31 | 29, 30 | eqtr4id 2796 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopSet‘𝐾)) |
| 32 | | utopbas 24244 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → 𝑋 = ∪
(unifTop‘𝑈)) |
| 33 | 31 | unieqd 4920 |
. . . . . 6
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (unifTop‘𝑈) = ∪
(TopSet‘𝐾)) |
| 34 | 32, 18, 33 | 3eqtr3rd 2786 |
. . . . 5
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ∪ (TopSet‘𝐾) = (Base‘𝐾)) |
| 35 | 34 | oveq2d 7447 |
. . . 4
⊢ (𝑈 ∈ (UnifOn‘𝑋) → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = ((TopSet‘𝐾) ↾t (Base‘𝐾))) |
| 36 | | fvex 6919 |
. . . . 5
⊢
(TopSet‘𝐾)
∈ V |
| 37 | | eqid 2737 |
. . . . . 6
⊢ ∪ (TopSet‘𝐾) = ∪
(TopSet‘𝐾) |
| 38 | 37 | restid 17478 |
. . . . 5
⊢
((TopSet‘𝐾)
∈ V → ((TopSet‘𝐾) ↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾)) |
| 39 | 36, 38 | ax-mp 5 |
. . . 4
⊢
((TopSet‘𝐾)
↾t ∪ (TopSet‘𝐾)) = (TopSet‘𝐾) |
| 40 | | eqid 2737 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 41 | | eqid 2737 |
. . . . 5
⊢
(TopSet‘𝐾) =
(TopSet‘𝐾) |
| 42 | 40, 41 | topnval 17479 |
. . . 4
⊢
((TopSet‘𝐾)
↾t (Base‘𝐾)) = (TopOpen‘𝐾) |
| 43 | 35, 39, 42 | 3eqtr3g 2800 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (TopSet‘𝐾) = (TopOpen‘𝐾)) |
| 44 | 31, 43 | eqtrd 2777 |
. 2
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (unifTop‘𝑈) = (TopOpen‘𝐾)) |
| 45 | 18, 24, 44 | 3jca 1129 |
1
⊢ (𝑈 ∈ (UnifOn‘𝑋) → (𝑋 = (Base‘𝐾) ∧ 𝑈 = (UnifSet‘𝐾) ∧ (unifTop‘𝑈) = (TopOpen‘𝐾))) |