Step | Hyp | Ref
| Expression |
1 | | elex 3243 |
. 2
⊢ (𝑊 ∈ UnifSp → 𝑊 ∈ V) |
2 | | 0nep0 4866 |
. . . . 5
⊢ ∅
≠ {∅} |
3 | | isusp.1 |
. . . . . . . . . . . 12
⊢ 𝐵 = (Base‘𝑊) |
4 | | fvprc 6223 |
. . . . . . . . . . . 12
⊢ (¬
𝑊 ∈ V →
(Base‘𝑊) =
∅) |
5 | 3, 4 | syl5eq 2697 |
. . . . . . . . . . 11
⊢ (¬
𝑊 ∈ V → 𝐵 = ∅) |
6 | 5 | fveq2d 6233 |
. . . . . . . . . 10
⊢ (¬
𝑊 ∈ V →
(UnifOn‘𝐵) =
(UnifOn‘∅)) |
7 | | ust0 22070 |
. . . . . . . . . 10
⊢
(UnifOn‘∅) = {{∅}} |
8 | 6, 7 | syl6eq 2701 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(UnifOn‘𝐵) =
{{∅}}) |
9 | 8 | eleq2d 2716 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → (𝑈 ∈ (UnifOn‘𝐵) ↔ 𝑈 ∈ {{∅}})) |
10 | | isusp.2 |
. . . . . . . . . 10
⊢ 𝑈 = (UnifSt‘𝑊) |
11 | | fvex 6239 |
. . . . . . . . . 10
⊢
(UnifSt‘𝑊)
∈ V |
12 | 10, 11 | eqeltri 2726 |
. . . . . . . . 9
⊢ 𝑈 ∈ V |
13 | 12 | elsn 4225 |
. . . . . . . 8
⊢ (𝑈 ∈ {{∅}} ↔ 𝑈 = {∅}) |
14 | 9, 13 | syl6bb 276 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → (𝑈 ∈ (UnifOn‘𝐵) ↔ 𝑈 = {∅})) |
15 | | fvprc 6223 |
. . . . . . . . 9
⊢ (¬
𝑊 ∈ V →
(UnifSt‘𝑊) =
∅) |
16 | 10, 15 | syl5eq 2697 |
. . . . . . . 8
⊢ (¬
𝑊 ∈ V → 𝑈 = ∅) |
17 | 16 | eqeq1d 2653 |
. . . . . . 7
⊢ (¬
𝑊 ∈ V → (𝑈 = {∅} ↔ ∅ =
{∅})) |
18 | 14, 17 | bitrd 268 |
. . . . . 6
⊢ (¬
𝑊 ∈ V → (𝑈 ∈ (UnifOn‘𝐵) ↔ ∅ =
{∅})) |
19 | 18 | necon3bbid 2860 |
. . . . 5
⊢ (¬
𝑊 ∈ V → (¬
𝑈 ∈
(UnifOn‘𝐵) ↔
∅ ≠ {∅})) |
20 | 2, 19 | mpbiri 248 |
. . . 4
⊢ (¬
𝑊 ∈ V → ¬
𝑈 ∈
(UnifOn‘𝐵)) |
21 | 20 | con4i 113 |
. . 3
⊢ (𝑈 ∈ (UnifOn‘𝐵) → 𝑊 ∈ V) |
22 | 21 | adantr 480 |
. 2
⊢ ((𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)) → 𝑊 ∈ V) |
23 | | fveq2 6229 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (UnifSt‘𝑤) = (UnifSt‘𝑊)) |
24 | 23, 10 | syl6eqr 2703 |
. . . . 5
⊢ (𝑤 = 𝑊 → (UnifSt‘𝑤) = 𝑈) |
25 | | fveq2 6229 |
. . . . . . 7
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = (Base‘𝑊)) |
26 | 25, 3 | syl6eqr 2703 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (Base‘𝑤) = 𝐵) |
27 | 26 | fveq2d 6233 |
. . . . 5
⊢ (𝑤 = 𝑊 → (UnifOn‘(Base‘𝑤)) = (UnifOn‘𝐵)) |
28 | 24, 27 | eleq12d 2724 |
. . . 4
⊢ (𝑤 = 𝑊 → ((UnifSt‘𝑤) ∈ (UnifOn‘(Base‘𝑤)) ↔ 𝑈 ∈ (UnifOn‘𝐵))) |
29 | | fveq2 6229 |
. . . . . 6
⊢ (𝑤 = 𝑊 → (TopOpen‘𝑤) = (TopOpen‘𝑊)) |
30 | | isusp.3 |
. . . . . 6
⊢ 𝐽 = (TopOpen‘𝑊) |
31 | 29, 30 | syl6eqr 2703 |
. . . . 5
⊢ (𝑤 = 𝑊 → (TopOpen‘𝑤) = 𝐽) |
32 | 24 | fveq2d 6233 |
. . . . 5
⊢ (𝑤 = 𝑊 → (unifTop‘(UnifSt‘𝑤)) = (unifTop‘𝑈)) |
33 | 31, 32 | eqeq12d 2666 |
. . . 4
⊢ (𝑤 = 𝑊 → ((TopOpen‘𝑤) = (unifTop‘(UnifSt‘𝑤)) ↔ 𝐽 = (unifTop‘𝑈))) |
34 | 28, 33 | anbi12d 747 |
. . 3
⊢ (𝑤 = 𝑊 → (((UnifSt‘𝑤) ∈ (UnifOn‘(Base‘𝑤)) ∧ (TopOpen‘𝑤) =
(unifTop‘(UnifSt‘𝑤))) ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))) |
35 | | df-usp 22108 |
. . 3
⊢ UnifSp =
{𝑤 ∣
((UnifSt‘𝑤) ∈
(UnifOn‘(Base‘𝑤)) ∧ (TopOpen‘𝑤) = (unifTop‘(UnifSt‘𝑤)))} |
36 | 34, 35 | elab2g 3385 |
. 2
⊢ (𝑊 ∈ V → (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈)))) |
37 | 1, 22, 36 | pm5.21nii 367 |
1
⊢ (𝑊 ∈ UnifSp ↔ (𝑈 ∈ (UnifOn‘𝐵) ∧ 𝐽 = (unifTop‘𝑈))) |