This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem repsf

Description: The constructed function mapping a half-open range of nonnegative integers to a constant is a function. (Contributed by AV, 4-Nov-2018)

Ref Expression
Assertion repsf 
|- ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) : ( 0 ..^ N ) --> V )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( S e. V /\ x e. ( 0 ..^ N ) ) -> S e. V )
2 1 ralrimiva 
 |-  ( S e. V -> A. x e. ( 0 ..^ N ) S e. V )
3 2 adantr 
 |-  ( ( S e. V /\ N e. NN0 ) -> A. x e. ( 0 ..^ N ) S e. V )
4 eqid 
 |-  ( x e. ( 0 ..^ N ) |-> S ) = ( x e. ( 0 ..^ N ) |-> S )
5 4 fmpt 
 |-  ( A. x e. ( 0 ..^ N ) S e. V <-> ( x e. ( 0 ..^ N ) |-> S ) : ( 0 ..^ N ) --> V )
6 3 5 sylib 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( x e. ( 0 ..^ N ) |-> S ) : ( 0 ..^ N ) --> V )
7 reps 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) = ( x e. ( 0 ..^ N ) |-> S ) )
8 7 feq1d 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( ( S repeatS N ) : ( 0 ..^ N ) --> V <-> ( x e. ( 0 ..^ N ) |-> S ) : ( 0 ..^ N ) --> V ) )
9 6 8 mpbird 
 |-  ( ( S e. V /\ N e. NN0 ) -> ( S repeatS N ) : ( 0 ..^ N ) --> V )