Metamath Proof Explorer


Theorem ismntop

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

Ref Expression
Assertion ismntop N 0 J V N ManTop J J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N

Proof

Step Hyp Ref Expression
1 ismntoplly N 0 J V N ManTop J J 2 nd 𝜔 J Haus J Locally TopOpen 𝔼 hil N
2 haustop J Haus J Top
3 2 adantl N 0 J Haus J Top
4 3 biantrurd N 0 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N J Top x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
5 hmpher Er Top
6 errel Er Top Rel
7 relelec Rel J 𝑡 u TopOpen 𝔼 hil N TopOpen 𝔼 hil N J 𝑡 u
8 5 6 7 mp2b J 𝑡 u TopOpen 𝔼 hil N TopOpen 𝔼 hil N J 𝑡 u
9 hmphsymb TopOpen 𝔼 hil N J 𝑡 u J 𝑡 u TopOpen 𝔼 hil N
10 8 9 bitr2i J 𝑡 u TopOpen 𝔼 hil N J 𝑡 u TopOpen 𝔼 hil N
11 10 a1i N 0 J Haus J 𝑡 u TopOpen 𝔼 hil N J 𝑡 u TopOpen 𝔼 hil N
12 11 anbi2d N 0 J Haus y u J 𝑡 u TopOpen 𝔼 hil N y u J 𝑡 u TopOpen 𝔼 hil N
13 12 rexbidv N 0 J Haus u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
14 13 2ralbidv N 0 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
15 islly J Locally TopOpen 𝔼 hil N J Top x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
16 15 a1i N 0 J Haus J Locally TopOpen 𝔼 hil N J Top x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
17 4 14 16 3bitr4rd N 0 J Haus J Locally TopOpen 𝔼 hil N x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
18 17 pm5.32da N 0 J Haus J Locally TopOpen 𝔼 hil N J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
19 18 anbi2d N 0 J 2 nd 𝜔 J Haus J Locally TopOpen 𝔼 hil N J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
20 3anass J 2 nd 𝜔 J Haus J Locally TopOpen 𝔼 hil N J 2 nd 𝜔 J Haus J Locally TopOpen 𝔼 hil N
21 3anass J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
22 19 20 21 3bitr4g N 0 J 2 nd 𝜔 J Haus J Locally TopOpen 𝔼 hil N J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
23 22 adantr N 0 J V J 2 nd 𝜔 J Haus J Locally TopOpen 𝔼 hil N J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N
24 1 23 bitrd N 0 J V N ManTop J J 2 nd 𝜔 J Haus x J y x u J 𝒫 x y u J 𝑡 u TopOpen 𝔼 hil N