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

Metamath Proof Explorer

Theorem oppfrcl3

Description: If an opposite functor of a class is a functor, then the second component of the original class must be a relation whose domain is a relation as well. (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 oppfrcl3 ⊢ φ → Rel ⁡ B ∧ Rel ⁡ dom ⁡ 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 oppfrcllem ⊢ φ → G ≠ ∅
13 11 12 eqnetrrd ⊢ φ → if Rel ⁡ B ∧ Rel ⁡ dom ⁡ B A tpos B ∅ ≠ ∅
14 iffalse ⊢ ¬ Rel ⁡ B ∧ Rel ⁡ dom ⁡ B → if Rel ⁡ B ∧ Rel ⁡ dom ⁡ B A tpos B ∅ = ∅
15 14 necon1ai ⊢ if Rel ⁡ B ∧ Rel ⁡ dom ⁡ B A tpos B ∅ ≠ ∅ → Rel ⁡ B ∧ Rel ⁡ dom ⁡ B
16 13 15 syl ⊢ φ → Rel ⁡ B ∧ Rel ⁡ dom ⁡ B