Metamath Proof Explorer

Theorem climfv

Description: The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion climfv 
|- ( F ~~> A -> A = ( ~~> ` F ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( F ~~> A -> F ~~> A )
2 climrel 
 |-  Rel ~~>
3 2 a1i 
 |-  ( F ~~> A -> Rel ~~> )
4 brrelex1 
 |-  ( ( Rel ~~> /\ F ~~> A ) -> F e. _V )
5 3 1 4 syl2anc 
 |-  ( F ~~> A -> F e. _V )
6 brrelex2 
 |-  ( ( Rel ~~> /\ F ~~> A ) -> A e. _V )
7 3 1 6 syl2anc 
 |-  ( F ~~> A -> A e. _V )
8 breldmg 
 |-  ( ( F e. _V /\ A e. _V /\ F ~~> A ) -> F e. dom ~~> )
9 5 7 1 8 syl3anc 
 |-  ( F ~~> A -> F e. dom ~~> )
10 climdm 
 |-  ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
11 9 10 sylib 
 |-  ( F ~~> A -> F ~~> ( ~~> ` F ) )
12 climuni 
 |-  ( ( F ~~> A /\ F ~~> ( ~~> ` F ) ) -> A = ( ~~> ` F ) )
13 1 11 12 syl2anc 
 |-  ( F ~~> A -> A = ( ~~> ` F ) )