Theorem fsuppcolem

Description: Lemma for fsuppco . Formula building theorem for finite supports: rearranging the index set. (Contributed by Stefan O'Rear, 21-Mar-2015)

	Ref	Expression
Hypotheses	fsuppcolem.f	|- ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
	fsuppcolem.g	|- ( ph -> G : X -1-1-> Y )
Assertion	fsuppcolem	|- ( ph -> ( `' ( F o. G ) " ( _V \ { Z } ) ) e. Fin )

Proof

Step	Hyp	Ref	Expression
1		fsuppcolem.f	|- ( ph -> ( `' F " ( _V \ { Z } ) ) e. Fin )
2		fsuppcolem.g	|- ( ph -> G : X -1-1-> Y )
3		cnvco	|- `' ( F o. G ) = ( `' G o. `' F )
4	3	imaeq1i	|- ( `' ( F o. G ) " ( _V \ { Z } ) ) = ( ( `' G o. `' F ) " ( _V \ { Z } ) )
5		imaco	|- ( ( `' G o. `' F ) " ( _V \ { Z } ) ) = ( `' G " ( `' F " ( _V \ { Z } ) ) )
6	4 5	eqtri	|- ( `' ( F o. G ) " ( _V \ { Z } ) ) = ( `' G " ( `' F " ( _V \ { Z } ) ) )
7		df-f1	|- ( G : X -1-1-> Y <-> ( G : X --> Y /\ Fun `' G ) )
8	7	simprbi	|- ( G : X -1-1-> Y -> Fun `' G )
9	2 8	syl	|- ( ph -> Fun `' G )
10		imafi	|- ( ( Fun `' G /\ ( `' F " ( _V \ { Z } ) ) e. Fin ) -> ( `' G " ( `' F " ( _V \ { Z } ) ) ) e. Fin )
11	9 1 10	syl2anc	|- ( ph -> ( `' G " ( `' F " ( _V \ { Z } ) ) ) e. Fin )
12	6 11	eqeltrid	|- ( ph -> ( `' ( F o. G ) " ( _V \ { Z } ) ) e. Fin )