Metamath Proof Explorer


Theorem clsneinex

Description: If closure and neighborhoods functions are related, the neighborhoods function exists. (Contributed by RP, 27-Jun-2021)

Ref Expression
Hypotheses clsnei.o
|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
clsnei.p
|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
clsnei.d
|- D = ( P ` B )
clsnei.f
|- F = ( ~P B O B )
clsnei.h
|- H = ( F o. D )
clsnei.r
|- ( ph -> K H N )
Assertion clsneinex
|- ( ph -> N e. ( ~P ~P B ^m B ) )

Proof

Step Hyp Ref Expression
1 clsnei.o
 |-  O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) )
2 clsnei.p
 |-  P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
3 clsnei.d
 |-  D = ( P ` B )
4 clsnei.f
 |-  F = ( ~P B O B )
5 clsnei.h
 |-  H = ( F o. D )
6 clsnei.r
 |-  ( ph -> K H N )
7 3 5 6 clsneibex
 |-  ( ph -> B e. _V )
8 pwexg
 |-  ( B e. _V -> ~P B e. _V )
9 8 adantl
 |-  ( ( ph /\ B e. _V ) -> ~P B e. _V )
10 simpr
 |-  ( ( ph /\ B e. _V ) -> B e. _V )
11 1 9 10 4 fsovf1od
 |-  ( ( ph /\ B e. _V ) -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) )
12 f1ofn
 |-  ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> F Fn ( ~P B ^m ~P B ) )
13 11 12 syl
 |-  ( ( ph /\ B e. _V ) -> F Fn ( ~P B ^m ~P B ) )
14 2 3 10 dssmapf1od
 |-  ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) )
15 f1of
 |-  ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) )
16 14 15 syl
 |-  ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) )
17 6 adantr
 |-  ( ( ph /\ B e. _V ) -> K H N )
18 5 breqi
 |-  ( K H N <-> K ( F o. D ) N )
19 17 18 sylib
 |-  ( ( ph /\ B e. _V ) -> K ( F o. D ) N )
20 13 16 19 brcoffn
 |-  ( ( ph /\ B e. _V ) -> ( K D ( D ` K ) /\ ( D ` K ) F N ) )
21 7 20 mpdan
 |-  ( ph -> ( K D ( D ` K ) /\ ( D ` K ) F N ) )
22 21 simprd
 |-  ( ph -> ( D ` K ) F N )
23 1 4 22 ntrneinex
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )