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

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 ⊢ φ → G ∈ R
oppfrcl.2 ⊢ Rel ⁡ R
oppfrcl.3 No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
oppfrcl2.4 ⊢ φ → F = A B
Assertion oppf1st2nd ⊢ φ → G ∈ V × V ∧ 1 st ⁡ G = A ∧ 2 nd ⁡ G = tpos B

Proof

Step Hyp Ref Expression
1 oppfrcl.1 ⊢ φ → G ∈ R
2 oppfrcl.2 ⊢ Rel ⁡ R
3 oppfrcl.3 Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
4 oppfrcl2.4 ⊢ φ → F = A B
5 4 fveq2d Could not format ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. A , B >. ) ) : No typesetting found for |- ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. A , B >. ) ) with typecode |-
6 df-ov Could not format ( A oppFunc B ) = ( oppFunc ` <. A , B >. ) : No typesetting found for |- ( A oppFunc B ) = ( oppFunc ` <. A , B >. ) with typecode |-
7 5 3 6 3eqtr4g Could not format ( ph -> G = ( A oppFunc B ) ) : No typesetting found for |- ( ph -> G = ( A oppFunc B ) ) with typecode |-
8 1 2 3 4 oppfrcl2 ⊢ φ → A ∈ V ∧ B ∈ V
9 oppfvalg Could not format ( ( A e. _V /\ B e. _V ) -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) : No typesetting found for |- ( ( A e. _V /\ B e. _V ) -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) with typecode |-
10 8 9 syl Could not format ( ph -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) : No typesetting found for |- ( ph -> ( A oppFunc B ) = if ( ( Rel B /\ Rel dom B ) , <. A , tpos B >. , (/) ) ) with typecode |-
11 7 10 eqtrd ⊢ φ → G = if Rel ⁡ B ∧ Rel ⁡ dom ⁡ B A tpos B ∅
12 1 2 3 4 oppfrcl3 ⊢ φ → Rel ⁡ B ∧ Rel ⁡ dom ⁡ B
13 12 iftrued ⊢ φ → if Rel ⁡ B ∧ Rel ⁡ dom ⁡ B A tpos B ∅ = A tpos B
14 11 13 eqtrd ⊢ φ → G = A tpos B
15 8 simpld ⊢ φ → A ∈ V
16 tposexg ⊢ B ∈ V → tpos B ∈ V
17 8 16 simpl2im ⊢ φ → tpos B ∈ V
18 15 17 opelxpd ⊢ φ → A tpos B ∈ V × V
19 14 18 eqeltrd ⊢ φ → G ∈ V × V
20 14 fveq2d ⊢ φ → 1 st ⁡ G = 1 st ⁡ A tpos B
21 op1stg ⊢ A ∈ V ∧ tpos B ∈ V → 1 st ⁡ A tpos B = A
22 15 17 21 syl2anc ⊢ φ → 1 st ⁡ A tpos B = A
23 20 22 eqtrd ⊢ φ → 1 st ⁡ G = A
24 14 fveq2d ⊢ φ → 2 nd ⁡ G = 2 nd ⁡ A tpos B
25 op2ndg ⊢ A ∈ V ∧ tpos B ∈ V → 2 nd ⁡ A tpos B = tpos B
26 15 17 25 syl2anc ⊢ φ → 2 nd ⁡ A tpos B = tpos B
27 24 26 eqtrd ⊢ φ → 2 nd ⁡ G = tpos B
28 19 23 27 jca32 ⊢ φ → G ∈ V × V ∧ 1 st ⁡ G = A ∧ 2 nd ⁡ G = tpos B