| Step |
Hyp |
Ref |
Expression |
| 1 |
|
oppfrcl.1 |
|- ( ph -> G e. R ) |
| 2 |
|
oppfrcl.2 |
|- Rel R |
| 3 |
|
oppfrcl.3 |
|- G = ( oppFunc ` F ) |
| 4 |
|
oppfrcl2.4 |
|- ( ph -> F = <. A , B >. ) |
| 5 |
4
|
fveq2d |
|- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. A , B >. ) ) |
| 6 |
|
df-ov |
|- ( A oppFunc B ) = ( oppFunc ` <. A , B >. ) |
| 7 |
5 3 6
|
3eqtr4g |
|- ( ph -> G = ( A oppFunc B ) ) |
| 8 |
1 2 3 4
|
oppfrcl2 |
|- ( ph -> ( A e. _V /\ B e. _V ) ) |
| 9 |
|
oppfvalg |
|- ( ( A e. _V /\ B e. _V ) -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) |
| 10 |
8 9
|
syl |
|- ( ph -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) |
| 11 |
7 10
|
eqtrd |
|- ( ph -> G = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) |
| 12 |
1 2 3 4
|
oppfrcl3 |
|- ( ph -> ( Rel B /\ Rel dom B ) ) |
| 13 |
12
|
iftrued |
|- ( ph -> if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) = <. A , tpos B >. ) |
| 14 |
11 13
|
eqtrd |
|- ( ph -> G = <. A , tpos B >. ) |
| 15 |
8
|
simpld |
|- ( ph -> A e. _V ) |
| 16 |
|
tposexg |
|- ( B e. _V -> tpos B e. _V ) |
| 17 |
8 16
|
simpl2im |
|- ( ph -> tpos B e. _V ) |
| 18 |
15 17
|
opelxpd |
|- ( ph -> <. A , tpos B >. e. ( _V X. _V ) ) |
| 19 |
14 18
|
eqeltrd |
|- ( ph -> G e. ( _V X. _V ) ) |
| 20 |
14
|
fveq2d |
|- ( ph -> ( 1st ` G ) = ( 1st ` <. A , tpos B >. ) ) |
| 21 |
|
op1stg |
|- ( ( A e. _V /\ tpos B e. _V ) -> ( 1st ` <. A , tpos B >. ) = A ) |
| 22 |
15 17 21
|
syl2anc |
|- ( ph -> ( 1st ` <. A , tpos B >. ) = A ) |
| 23 |
20 22
|
eqtrd |
|- ( ph -> ( 1st ` G ) = A ) |
| 24 |
14
|
fveq2d |
|- ( ph -> ( 2nd ` G ) = ( 2nd ` <. A , tpos B >. ) ) |
| 25 |
|
op2ndg |
|- ( ( A e. _V /\ tpos B e. _V ) -> ( 2nd ` <. A , tpos B >. ) = tpos B ) |
| 26 |
15 17 25
|
syl2anc |
|- ( ph -> ( 2nd ` <. A , tpos B >. ) = tpos B ) |
| 27 |
24 26
|
eqtrd |
|- ( ph -> ( 2nd ` G ) = tpos B ) |
| 28 |
19 23 27
|
jca32 |
|- ( ph -> ( G e. ( _V X. _V ) /\ ( ( 1st ` G ) = A /\ ( 2nd ` G ) = tpos B ) ) ) |