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

Metamath Proof Explorer

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 )