Metamath Proof Explorer

Theorem ismntop

Description: Property of being a manifold. (Contributed by Thierry Arnoux, 5-Jan-2020)

Ref Expression
Assertion ismntop 
|- ( ( N e. NN0 /\ J e. V ) -> ( N ManTop J <-> ( J e. 2ndc /\ J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ismntoplly 
 |-  ( ( N e. NN0 /\ J e. V ) -> ( N ManTop J <-> ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
2 haustop 
 |-  ( J e. Haus -> J e. Top )
3 2 adantl 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> J e. Top )
4 3 biantrurd 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) ) )
5 hmpher 
 |-  ~= Er Top
6 errel 
 |-  ( ~= Er Top -> Rel ~= )
7 relelec 
 |-  ( Rel ~= -> ( ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= <-> ( TopOpen ` ( EEhil ` N ) ) ~= ( J |`t u ) ) )
8 5 6 7 mp2b 
 |-  ( ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= <-> ( TopOpen ` ( EEhil ` N ) ) ~= ( J |`t u ) )
9 hmphsymb 
 |-  ( ( TopOpen ` ( EEhil ` N ) ) ~= ( J |`t u ) <-> ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) )
10 8 9 bitr2i 
 |-  ( ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) <-> ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= )
11 10 a1i 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) <-> ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) )
12 11 anbi2d 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) <-> ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
13 12 rexbidv 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) <-> E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
14 13 2ralbidv 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) <-> A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
15 islly 
 |-  ( J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
16 15 a1i 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= <-> ( J e. Top /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) e. [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) ) )
17 4 14 16 3bitr4rd 
 |-  ( ( N e. NN0 /\ J e. Haus ) -> ( J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= <-> A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) )
18 17 pm5.32da 
 |-  ( N e. NN0 -> ( ( J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) <-> ( J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) )
19 18 anbi2d 
 |-  ( N e. NN0 -> ( ( J e. 2ndc /\ ( J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) <-> ( J e. 2ndc /\ ( J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) ) )
20 3anass 
 |-  ( ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) <-> ( J e. 2ndc /\ ( J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
21 3anass 
 |-  ( ( J e. 2ndc /\ J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) <-> ( J e. 2ndc /\ ( J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) )
22 19 20 21 3bitr4g 
 |-  ( N e. NN0 -> ( ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) <-> ( J e. 2ndc /\ J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) )
23 22 adantr 
 |-  ( ( N e. NN0 /\ J e. V ) -> ( ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) <-> ( J e. 2ndc /\ J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) )
24 1 23 bitrd 
 |-  ( ( N e. NN0 /\ J e. V ) -> ( N ManTop J <-> ( J e. 2ndc /\ J e. Haus /\ A. x e. J A. y e. x E. u e. ( J i^i ~P x ) ( y e. u /\ ( J |`t u ) ~= ( TopOpen ` ( EEhil ` N ) ) ) ) ) )