Metamath Proof Explorer

Theorem oppf1st2nd

Description: Rewrite the opposite functor into its components ( eqopi ). (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses oppfrcl.1 
|- ( ph -> G e. R )
oppfrcl.2 
|- Rel R
oppfrcl.3 
|- G = ( oppFunc ` F )
oppfrcl2.4 
|- ( ph -> F = <. A , B >. )
Assertion oppf1st2nd 
|- ( ph -> ( G e. ( _V X. _V ) /\ ( ( 1st ` G ) = A /\ ( 2nd ` G ) = tpos B ) ) )

Proof

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 ) ) )