Metamath Proof Explorer

Theorem ulmuni

Description: A sequence of functions uniformly converges to at most one limit. (Contributed by Mario Carneiro, 5-Jul-2017)

Ref Expression
Assertion ulmuni 
|- ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) -> G = H )

Proof

Step Hyp Ref Expression
1 ulmcl 
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
2 1 adantr 
 |-  ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) -> G : S --> CC )
3 2 ffnd 
 |-  ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) -> G Fn S )
4 ulmcl 
 |-  ( F ( ~~>u ` S ) H -> H : S --> CC )
5 4 adantl 
 |-  ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) -> H : S --> CC )
6 5 ffnd 
 |-  ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) -> H Fn S )
7 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
8 simplr 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> n e. ZZ )
9 simpr 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> F : ( ZZ>= ` n ) --> ( CC ^m S ) )
10 simpllr 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> x e. S )
11 fvex 
 |-  ( ZZ>= ` n ) e. _V
12 11 mptex 
 |-  ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) e. _V
13 12 a1i 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) e. _V )
14 fveq2 
 |-  ( i = k -> ( F ` i ) = ( F ` k ) )
15 14 fveq1d 
 |-  ( i = k -> ( ( F ` i ) ` x ) = ( ( F ` k ) ` x ) )
16 eqid 
 |-  ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) = ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) )
17 fvex 
 |-  ( ( F ` k ) ` x ) e. _V
18 15 16 17 fvmpt 
 |-  ( k e. ( ZZ>= ` n ) -> ( ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ` k ) = ( ( F ` k ) ` x ) )
19 18 eqcomd 
 |-  ( k e. ( ZZ>= ` n ) -> ( ( F ` k ) ` x ) = ( ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ` k ) )
20 19 adantl 
 |-  ( ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) /\ k e. ( ZZ>= ` n ) ) -> ( ( F ` k ) ` x ) = ( ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ` k ) )
21 simp-4l 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> F ( ~~>u ` S ) G )
22 7 8 9 10 13 20 21 ulmclm 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ~~> ( G ` x ) )
23 simp-4r 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> F ( ~~>u ` S ) H )
24 7 8 9 10 13 20 23 ulmclm 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ~~> ( H ` x ) )
25 climuni 
 |-  ( ( ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ~~> ( G ` x ) /\ ( i e. ( ZZ>= ` n ) |-> ( ( F ` i ) ` x ) ) ~~> ( H ` x ) ) -> ( G ` x ) = ( H ` x ) )
26 22 24 25 syl2anc 
 |-  ( ( ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) /\ n e. ZZ ) /\ F : ( ZZ>= ` n ) --> ( CC ^m S ) ) -> ( G ` x ) = ( H ` x ) )
27 ulmf 
 |-  ( F ( ~~>u ` S ) G -> E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) )
28 27 ad2antrr 
 |-  ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) -> E. n e. ZZ F : ( ZZ>= ` n ) --> ( CC ^m S ) )
29 26 28 r19.29a 
 |-  ( ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) /\ x e. S ) -> ( G ` x ) = ( H ` x ) )
30 3 6 29 eqfnfvd 
 |-  ( ( F ( ~~>u ` S ) G /\ F ( ~~>u ` S ) H ) -> G = H )