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	ffvelrnd	|- ( 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 ) ) >. } ) )