Metamath Proof Explorer

Theorem ismntoplly

Description: Property of being a manifold. (Contributed by Thierry Arnoux, 28-Dec-2019)

Ref Expression
Assertion ismntoplly 
|- ( ( N e. NN0 /\ J e. V ) -> ( N ManTop J <-> ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN0 /\ J e. V ) -> N e. NN0 )
2 simpl 
 |-  ( ( n = N /\ j = J ) -> n = N )
3 2 eleq1d 
 |-  ( ( n = N /\ j = J ) -> ( n e. NN0 <-> N e. NN0 ) )
4 simpr 
 |-  ( ( n = N /\ j = J ) -> j = J )
5 4 eleq1d 
 |-  ( ( n = N /\ j = J ) -> ( j e. 2ndc <-> J e. 2ndc ) )
6 4 eleq1d 
 |-  ( ( n = N /\ j = J ) -> ( j e. Haus <-> J e. Haus ) )
7 2fveq3 
 |-  ( n = N -> ( TopOpen ` ( EEhil ` n ) ) = ( TopOpen ` ( EEhil ` N ) ) )
8 7 eceq1d 
 |-  ( n = N -> [ ( TopOpen ` ( EEhil ` n ) ) ] ~= = [ ( TopOpen ` ( EEhil ` N ) ) ] ~= )
9 llyeq 
 |-  ( [ ( TopOpen ` ( EEhil ` n ) ) ] ~= = [ ( TopOpen ` ( EEhil ` N ) ) ] ~= -> Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= = Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= )
10 8 9 syl 
 |-  ( n = N -> Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= = Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= )
11 10 adantr 
 |-  ( ( n = N /\ j = J ) -> Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= = Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= )
12 4 11 eleq12d 
 |-  ( ( n = N /\ j = J ) -> ( j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= <-> J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) )
13 5 6 12 3anbi123d 
 |-  ( ( n = N /\ j = J ) -> ( ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) <-> ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )
14 3 13 anbi12d 
 |-  ( ( n = N /\ j = J ) -> ( ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) <-> ( N e. NN0 /\ ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) ) )
15 df-mntop 
 |-  ManTop = { <. n , j >. | ( n e. NN0 /\ ( j e. 2ndc /\ j e. Haus /\ j e. Locally [ ( TopOpen ` ( EEhil ` n ) ) ] ~= ) ) }
16 14 15 brabga 
 |-  ( ( N e. NN0 /\ J e. V ) -> ( N ManTop J <-> ( N e. NN0 /\ ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) ) )
17 1 16 mpbirand 
 |-  ( ( N e. NN0 /\ J e. V ) -> ( N ManTop J <-> ( J e. 2ndc /\ J e. Haus /\ J e. Locally [ ( TopOpen ` ( EEhil ` N ) ) ] ~= ) ) )