Step |
Hyp |
Ref |
Expression |
1 |
|
df-ov |
|- ( I e.g J ) = ( e.g ` <. I , J >. ) |
2 |
|
df-goel |
|- e.g = ( x e. ( _om X. _om ) |-> <. (/) , x >. ) |
3 |
2
|
a1i |
|- ( ( I e. _om /\ J e. _om ) -> e.g = ( x e. ( _om X. _om ) |-> <. (/) , x >. ) ) |
4 |
|
opeq2 |
|- ( x = <. I , J >. -> <. (/) , x >. = <. (/) , <. I , J >. >. ) |
5 |
4
|
adantl |
|- ( ( ( I e. _om /\ J e. _om ) /\ x = <. I , J >. ) -> <. (/) , x >. = <. (/) , <. I , J >. >. ) |
6 |
|
opelxpi |
|- ( ( I e. _om /\ J e. _om ) -> <. I , J >. e. ( _om X. _om ) ) |
7 |
|
opex |
|- <. (/) , <. I , J >. >. e. _V |
8 |
7
|
a1i |
|- ( ( I e. _om /\ J e. _om ) -> <. (/) , <. I , J >. >. e. _V ) |
9 |
3 5 6 8
|
fvmptd |
|- ( ( I e. _om /\ J e. _om ) -> ( e.g ` <. I , J >. ) = <. (/) , <. I , J >. >. ) |
10 |
1 9
|
syl5eq |
|- ( ( I e. _om /\ J e. _om ) -> ( I e.g J ) = <. (/) , <. I , J >. >. ) |