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

Metamath Proof Explorer

Theorem seqomeq12

Description: Equality theorem for seqom . (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Assertion seqomeq12 
|- ( ( A = B /\ C = D ) -> seqom ( A , C ) = seqom ( B , D ) )

Proof

Step Hyp Ref Expression
1 oveq 
 |-  ( A = B -> ( a A b ) = ( a B b ) )
2 1 opeq2d 
 |-  ( A = B -> <. suc a , ( a A b ) >. = <. suc a , ( a B b ) >. )
3 2 mpoeq3dv 
 |-  ( A = B -> ( a e. _om , b e. _V |-> <. suc a , ( a A b ) >. ) = ( a e. _om , b e. _V |-> <. suc a , ( a B b ) >. ) )
4 fveq2 
 |-  ( C = D -> ( _I ` C ) = ( _I ` D ) )
5 4 opeq2d 
 |-  ( C = D -> <. (/) , ( _I ` C ) >. = <. (/) , ( _I ` D ) >. )
6 rdgeq12 
 |-  ( ( ( a e. _om , b e. _V |-> <. suc a , ( a A b ) >. ) = ( a e. _om , b e. _V |-> <. suc a , ( a B b ) >. ) /\ <. (/) , ( _I ` C ) >. = <. (/) , ( _I ` D ) >. ) -> rec ( ( a e. _om , b e. _V |-> <. suc a , ( a A b ) >. ) , <. (/) , ( _I ` C ) >. ) = rec ( ( a e. _om , b e. _V |-> <. suc a , ( a B b ) >. ) , <. (/) , ( _I ` D ) >. ) )
7 3 5 6 syl2an 
 |-  ( ( A = B /\ C = D ) -> rec ( ( a e. _om , b e. _V |-> <. suc a , ( a A b ) >. ) , <. (/) , ( _I ` C ) >. ) = rec ( ( a e. _om , b e. _V |-> <. suc a , ( a B b ) >. ) , <. (/) , ( _I ` D ) >. ) )
8 7 imaeq1d 
 |-  ( ( A = B /\ C = D ) -> ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a A b ) >. ) , <. (/) , ( _I ` C ) >. ) " _om ) = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a B b ) >. ) , <. (/) , ( _I ` D ) >. ) " _om ) )
9 df-seqom 
 |-  seqom ( A , C ) = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a A b ) >. ) , <. (/) , ( _I ` C ) >. ) " _om )
10 df-seqom 
 |-  seqom ( B , D ) = ( rec ( ( a e. _om , b e. _V |-> <. suc a , ( a B b ) >. ) , <. (/) , ( _I ` D ) >. ) " _om )
11 8 9 10 3eqtr4g 
 |-  ( ( A = B /\ C = D ) -> seqom ( A , C ) = seqom ( B , D ) )