Metamath Proof Explorer

Theorem isusp

Description: The predicate W is a uniform space. (Contributed by Thierry Arnoux, 4-Dec-2017)

Ref Expression
Hypotheses isusp.1 ⊢ B = Base W
isusp.2 ⊢ U = UnifSt ⁡ W
isusp.3 ⊢ J = TopOpen ⁡ W
Assertion isusp ⊢ W ∈ UnifSp ↔ U ∈ UnifOn ⁡ B ∧ J = unifTop ⁡ U

Proof

Step Hyp Ref Expression
1 isusp.1 ⊢ B = Base W
2 isusp.2 ⊢ U = UnifSt ⁡ W
3 isusp.3 ⊢ J = TopOpen ⁡ W
4 elex ⊢ W ∈ UnifSp → W ∈ V
5 0nep0 ⊢ ∅ ≠ ∅
6 fvprc ⊢ ¬ W ∈ V → Base W = ∅
7 1 6 eqtrid ⊢ ¬ W ∈ V → B = ∅
8 7 fveq2d ⊢ ¬ W ∈ V → UnifOn ⁡ B = UnifOn ⁡ ∅
9 ust0 ⊢ UnifOn ⁡ ∅ = ∅
10 8 9 eqtrdi ⊢ ¬ W ∈ V → UnifOn ⁡ B = ∅
11 10 eleq2d ⊢ ¬ W ∈ V → U ∈ UnifOn ⁡ B ↔ U ∈ ∅
12 2 fvexi ⊢ U ∈ V
13 12 elsn ⊢ U ∈ ∅ ↔ U = ∅
14 11 13 bitrdi ⊢ ¬ W ∈ V → U ∈ UnifOn ⁡ B ↔ U = ∅
15 fvprc ⊢ ¬ W ∈ V → UnifSt ⁡ W = ∅
16 2 15 eqtrid ⊢ ¬ W ∈ V → U = ∅
17 16 eqeq1d ⊢ ¬ W ∈ V → U = ∅ ↔ ∅ = ∅
18 14 17 bitrd ⊢ ¬ W ∈ V → U ∈ UnifOn ⁡ B ↔ ∅ = ∅
19 18 necon3bbid ⊢ ¬ W ∈ V → ¬ U ∈ UnifOn ⁡ B ↔ ∅ ≠ ∅
20 5 19 mpbiri ⊢ ¬ W ∈ V → ¬ U ∈ UnifOn ⁡ B
21 20 con4i ⊢ U ∈ UnifOn ⁡ B → W ∈ V
22 21 adantr ⊢ U ∈ UnifOn ⁡ B ∧ J = unifTop ⁡ U → W ∈ V
23 fveq2 ⊢ w = W → UnifSt ⁡ w = UnifSt ⁡ W
24 23 2 eqtr4di ⊢ w = W → UnifSt ⁡ w = U
25 fveq2 ⊢ w = W → Base w = Base W
26 25 1 eqtr4di ⊢ w = W → Base w = B
27 26 fveq2d ⊢ w = W → UnifOn ⁡ Base w = UnifOn ⁡ B
28 24 27 eleq12d ⊢ w = W → UnifSt ⁡ w ∈ UnifOn ⁡ Base w ↔ U ∈ UnifOn ⁡ B
29 fveq2 ⊢ w = W → TopOpen ⁡ w = TopOpen ⁡ W
30 29 3 eqtr4di ⊢ w = W → TopOpen ⁡ w = J
31 24 fveq2d ⊢ w = W → unifTop ⁡ UnifSt ⁡ w = unifTop ⁡ U
32 30 31 eqeq12d ⊢ w = W → TopOpen ⁡ w = unifTop ⁡ UnifSt ⁡ w ↔ J = unifTop ⁡ U
33 28 32 anbi12d ⊢ w = W → UnifSt ⁡ w ∈ UnifOn ⁡ Base w ∧ TopOpen ⁡ w = unifTop ⁡ UnifSt ⁡ w ↔ U ∈ UnifOn ⁡ B ∧ J = unifTop ⁡ U
34 df-usp ⊢ UnifSp = w | UnifSt ⁡ w ∈ UnifOn ⁡ Base w ∧ TopOpen ⁡ w = unifTop ⁡ UnifSt ⁡ w
35 33 34 elab2g ⊢ W ∈ V → W ∈ UnifSp ↔ U ∈ UnifOn ⁡ B ∧ J = unifTop ⁡ U
36 4 22 35 pm5.21nii ⊢ W ∈ UnifSp ↔ U ∈ UnifOn ⁡ B ∧ J = unifTop ⁡ U