Metamath Proof Explorer

Theorem neicvgfv

Description: The value of the neighborhoods (convergents) in terms of the the convergents (neighborhoods) function. (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 )
neicvgfv.x 
|- ( ph -> X e. B )
Assertion neicvgfv 
|- ( ph -> ( N ` X ) = { s e. ~P B | -. ( B \ s ) e. ( M ` X ) } )

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 neicvgfv.x 
 |-  ( ph -> X e. B )
9 dfin5 
 |-  ( ~P B i^i ( N ` X ) ) = { s e. ~P B | s e. ( N ` X ) }
10 1 2 3 4 5 6 7 neicvgnex 
 |-  ( ph -> N e. ( ~P ~P B ^m B ) )
11 elmapi 
 |-  ( N e. ( ~P ~P B ^m B ) -> N : B --> ~P ~P B )
12 10 11 syl 
 |-  ( ph -> N : B --> ~P ~P B )
13 12 8 ffvelrnd 
 |-  ( ph -> ( N ` X ) e. ~P ~P B )
14 13 elpwid 
 |-  ( ph -> ( N ` X ) C_ ~P B )
15 sseqin2 
 |-  ( ( N ` X ) C_ ~P B <-> ( ~P B i^i ( N ` X ) ) = ( N ` X ) )
16 14 15 sylib 
 |-  ( ph -> ( ~P B i^i ( N ` X ) ) = ( N ` X ) )
17 7 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> N H M )
18 8 adantr 
 |-  ( ( ph /\ s e. ~P B ) -> X e. B )
19 simpr 
 |-  ( ( ph /\ s e. ~P B ) -> s e. ~P B )
20 1 2 3 4 5 6 17 18 19 neicvgel1 
 |-  ( ( ph /\ s e. ~P B ) -> ( s e. ( N ` X ) <-> -. ( B \ s ) e. ( M ` X ) ) )
21 20 rabbidva 
 |-  ( ph -> { s e. ~P B | s e. ( N ` X ) } = { s e. ~P B | -. ( B \ s ) e. ( M ` X ) } )
22 9 16 21 3eqtr3a 
 |-  ( ph -> ( N ` X ) = { s e. ~P B | -. ( B \ s ) e. ( M ` X ) } )