| Step | Hyp | Ref
| Expression |
| 1 | | elex 3501 |
. 2
⊢ (𝑊 ∈ UnifSp → 𝑊 ∈ V) |
| 2 | | 0nep0 5358 |
. . . . 5
⊢ ∅
≠ {∅} |
| 3 | | isusp.1 |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑊) |
| 4 | | fvprc 6898 |
. . . . . . . . . . . 12
⊢ (¬
𝑊 ∈ V →
(Base‘𝑊) =
∅) |
| 5 | 3, 4 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ (¬
𝑊 ∈ V → 𝐵 = ∅) |
| 6 | 5 | fveq2d 6910 |
. . . . . . . . . 10
⊢ (¬
𝑊 ∈ V →
(UnifOn‘𝐵) =
(UnifOn‘∅)) |
| 7 | | ust0 24228 |
. . . . . . . . . 10
⊢
(UnifOn‘∅) = {{∅}} |
| 8 | 6, 7 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(UnifOn‘𝐵) =
{{∅}}) |
| 9 | 8 | eleq2d 2827 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → (𝑈 ∈ (UnifOn‘𝐵) ↔ 𝑈 ∈ {{∅}})) |
| 10 | | isusp.2 |
. . . . . . . . . 10
⊢ 𝑈 = (UnifSt‘𝑊) |
| 11 | 10 | fvexi 6920 |
. . . . . . . . 9
⊢ 𝑈 ∈ V |
| 12 | 11 | elsn 4641 |
. . . . . . . 8
⊢ (𝑈 ∈ {{∅}} ↔ 𝑈 = {∅}) |
| 13 | 9, 12 | bitrdi 287 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → (𝑈 ∈ (UnifOn‘𝐵) ↔ 𝑈 = {∅})) |
| 14 | | fvprc 6898 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(UnifSt‘𝑊) =
∅) |
| 15 | 10, 14 | eqtrid 2789 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → 𝑈 = ∅) |
| 16 | 15 | eqeq1d 2739 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → (𝑈 = {∅} ↔ ∅ =
{∅})) |
| 17 | 13, 16 | bitrd 279 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → (𝑈 ∈ (UnifOn‘𝐵) ↔ ∅ =
{∅})) |
| 18 | 17 | necon3bbid 2978 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (¬
𝑈 ∈
(UnifOn‘𝐵) ↔
∅ ≠ {∅})) |
| 19 | 2, 18 | mpbiri 258 |
. . . 4
⊢ (¬
𝑊 ∈ V → ¬
𝑈 ∈
(UnifOn‘𝐵)) |
| 20 | 19 | con4i 114 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝐵) → 𝑊 ∈ V) |
| 21 | 20 | adantr 480 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)) → 𝑊 ∈ V) |
| 22 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (UnifSt‘𝑤) = (UnifSt‘𝑊)) |
| 23 | 22, 10 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → (UnifSt‘𝑤) = 𝑈) |
| 24 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
| 25 | 24, 3 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) |
| 26 | 25 | fveq2d 6910 |
. . . . 5
⊢ (𝑤 = 𝑊 → (UnifOn‘(Base‘𝑤)) = (UnifOn‘𝐵)) |
| 27 | 23, 26 | eleq12d 2835 |
. . . 4
⊢ (𝑤 = 𝑊 → ((UnifSt‘𝑤) ∈ (UnifOn‘(Base‘𝑤)) ↔ 𝑈 ∈ (UnifOn‘𝐵))) |
| 28 | | fveq2 6906 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (TopOpen‘𝑤) = (TopOpen‘𝑊)) |
| 29 | | isusp.3 |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝑊) |
| 30 | 28, 29 | eqtr4di 2795 |
. . . . 5
⊢ (𝑤 = 𝑊 → (TopOpen‘𝑤) = 𝐽) |
| 31 | 23 | fveq2d 6910 |
. . . . 5
⊢ (𝑤 = 𝑊 → (unifTop‘(UnifSt‘𝑤)) = (unifTop‘𝑈)) |
| 32 | 30, 31 | eqeq12d 2753 |
. . . 4
⊢ (𝑤 = 𝑊 → ((TopOpen‘𝑤) = (unifTop‘(UnifSt‘𝑤)) ↔ 𝐽 = (unifTop‘𝑈))) |
| 33 | 27, 32 | anbi12d 632 |
. . 3
⊢ (𝑤 = 𝑊 → (((UnifSt‘𝑤) ∈ (UnifOn‘(Base‘𝑤)) ∧ (TopOpen‘𝑤) =
(unifTop‘(UnifSt‘𝑤))) ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))) |
| 34 | | df-usp 24266 |
. . 3
⊢ UnifSp =
{𝑤 ∣
((UnifSt‘𝑤) ∈
(UnifOn‘(Base‘𝑤)) ∧ (TopOpen‘𝑤) = (unifTop‘(UnifSt‘𝑤)))} |
| 35 | 33, 34 | elab2g 3680 |
. 2
⊢ (𝑊 ∈ V → (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))) |
| 36 | 1, 21, 35 | pm5.21nii 378 |
1
⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈))) |