Metamath Proof Explorer

Theorem algrflem

Description: Lemma for algrf and related theorems. (Contributed by Mario Carneiro, 28-May-2014) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Hypotheses algrflem.1 
|- B e. _V
algrflem.2 
|- C e. _V
Assertion algrflem 
|- ( B ( F o. 1st ) C ) = ( F ` B )

Proof

Step Hyp Ref Expression
1 algrflem.1 
 |-  B e. _V
2 algrflem.2 
 |-  C e. _V
3 df-ov 
 |-  ( B ( F o. 1st ) C ) = ( ( F o. 1st ) ` <. B , C >. )
4 fo1st 
 |-  1st : _V -onto-> _V
5 fof 
 |-  ( 1st : _V -onto-> _V -> 1st : _V --> _V )
6 4 5 ax-mp 
 |-  1st : _V --> _V
7 opex 
 |-  <. B , C >. e. _V
8 fvco3 
 |-  ( ( 1st : _V --> _V /\ <. B , C >. e. _V ) -> ( ( F o. 1st ) ` <. B , C >. ) = ( F ` ( 1st ` <. B , C >. ) ) )
9 6 7 8 mp2an 
 |-  ( ( F o. 1st ) ` <. B , C >. ) = ( F ` ( 1st ` <. B , C >. ) )
10 1 2 op1st 
 |-  ( 1st ` <. B , C >. ) = B
11 10 fveq2i 
 |-  ( F ` ( 1st ` <. B , C >. ) ) = ( F ` B )
12 3 9 11 3eqtri 
 |-  ( B ( F o. 1st ) C ) = ( F ` B )