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

Metamath Proof Explorer

Theorem repsundef

Description: A function mapping a half-open range of nonnegative integers with an upper bound not being a nonnegative integer to a constant is the empty set (in the meaning of "undefined"). (Contributed by AV, 5-Nov-2018)

Ref Expression
Assertion repsundef 
|- ( N e/ NN0 -> ( S repeatS N ) = (/) )

Proof

Step Hyp Ref Expression
1 df-reps 
 |-  repeatS = ( s e. _V , n e. NN0 |-> ( x e. ( 0 ..^ n ) |-> s ) )
2 ovex 
 |-  ( 0 ..^ n ) e. _V
3 2 mptex 
 |-  ( x e. ( 0 ..^ n ) |-> s ) e. _V
4 1 3 dmmpo 
 |-  dom repeatS = ( _V X. NN0 )
5 df-nel 
 |-  ( N e/ NN0 <-> -. N e. NN0 )
6 5 biimpi 
 |-  ( N e/ NN0 -> -. N e. NN0 )
7 6 intnand 
 |-  ( N e/ NN0 -> -. ( S e. _V /\ N e. NN0 ) )
8 ndmovg 
 |-  ( ( dom repeatS = ( _V X. NN0 ) /\ -. ( S e. _V /\ N e. NN0 ) ) -> ( S repeatS N ) = (/) )
9 4 7 8 sylancr 
 |-  ( N e/ NN0 -> ( S repeatS N ) = (/) )