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

Metamath Proof Explorer

Theorem resunimafz0

Description: TODO-AV: Revise using F e. Word dom I ? Formerly part of proof of eupth2lem3 : The union of a restriction by an image over an open range of nonnegative integers and a singleton of an ordered pair is a restriction by an image over an interval of nonnegative integers. (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 20-Feb-2021)

Ref Expression
Hypotheses resunimafz0.i 
|- ( ph -> Fun I )
resunimafz0.f 
|- ( ph -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
resunimafz0.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
Assertion resunimafz0 
|- ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )

Proof

Step Hyp Ref Expression
1 resunimafz0.i 
 |-  ( ph -> Fun I )
2 resunimafz0.f 
 |-  ( ph -> F : ( 0 ..^ ( # ` F ) ) --> dom I )
3 resunimafz0.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
4 imaundi 
 |-  ( F " ( ( 0 ..^ N ) u. { N } ) ) = ( ( F " ( 0 ..^ N ) ) u. ( F " { N } ) )
5 elfzonn0 
 |-  ( N e. ( 0 ..^ ( # ` F ) ) -> N e. NN0 )
6 3 5 syl 
 |-  ( ph -> N e. NN0 )
7 elnn0uz 
 |-  ( N e. NN0 <-> N e. ( ZZ>= ` 0 ) )
8 6 7 sylib 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
9 fzisfzounsn 
 |-  ( N e. ( ZZ>= ` 0 ) -> ( 0 ... N ) = ( ( 0 ..^ N ) u. { N } ) )
10 8 9 syl 
 |-  ( ph -> ( 0 ... N ) = ( ( 0 ..^ N ) u. { N } ) )
11 10 imaeq2d 
 |-  ( ph -> ( F " ( 0 ... N ) ) = ( F " ( ( 0 ..^ N ) u. { N } ) ) )
12 2 ffnd 
 |-  ( ph -> F Fn ( 0 ..^ ( # ` F ) ) )
13 fnsnfv 
 |-  ( ( F Fn ( 0 ..^ ( # ` F ) ) /\ N e. ( 0 ..^ ( # ` F ) ) ) -> { ( F ` N ) } = ( F " { N } ) )
14 12 3 13 syl2anc 
 |-  ( ph -> { ( F ` N ) } = ( F " { N } ) )
15 14 uneq2d 
 |-  ( ph -> ( ( F " ( 0 ..^ N ) ) u. { ( F ` N ) } ) = ( ( F " ( 0 ..^ N ) ) u. ( F " { N } ) ) )
16 4 11 15 3eqtr4a 
 |-  ( ph -> ( F " ( 0 ... N ) ) = ( ( F " ( 0 ..^ N ) ) u. { ( F ` N ) } ) )
17 16 reseq2d 
 |-  ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( I |` ( ( F " ( 0 ..^ N ) ) u. { ( F ` N ) } ) ) )
18 resundi 
 |-  ( I |` ( ( F " ( 0 ..^ N ) ) u. { ( F ` N ) } ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. ( I |` { ( F ` N ) } ) )
19 17 18 eqtrdi 
 |-  ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. ( I |` { ( F ` N ) } ) ) )
20 1 funfnd 
 |-  ( ph -> I Fn dom I )
21 2 3 ffvelcdmd 
 |-  ( ph -> ( F ` N ) e. dom I )
22 fnressn 
 |-  ( ( I Fn dom I /\ ( F ` N ) e. dom I ) -> ( I |` { ( F ` N ) } ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
23 20 21 22 syl2anc 
 |-  ( ph -> ( I |` { ( F ` N ) } ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )
24 23 uneq2d 
 |-  ( ph -> ( ( I |` ( F " ( 0 ..^ N ) ) ) u. ( I |` { ( F ` N ) } ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )
25 19 24 eqtrd 
 |-  ( ph -> ( I |` ( F " ( 0 ... N ) ) ) = ( ( I |` ( F " ( 0 ..^ N ) ) ) u. { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) )