Theorem neicvgnex

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

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

Proof

Step	Hyp	Ref	Expression
1		neicvg.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		neicvg.p	|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) )
3		neicvg.d	|- D = ( P ` B )
4		neicvg.f	|- F = ( ~P B O B )
5		neicvg.g	|- G = ( B O ~P B )
6		neicvg.h	|- H = ( F o. ( D o. G ) )
7		neicvg.r	|- ( ph -> N H M )
8	1 2 3 4 5 6 7	neicvgnvor	|- ( ph -> M H N )
9	1 2 3 4 5 6 8	neicvgmex	|- ( ph -> N e. ( ~P ~P B ^m B ) )