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 ⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
oppfrcl.2 ⊢ Rel 𝑅
oppfrcl.3 ⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
oppfrcl2.4 ⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
Assertion oppfrcl3 ( 𝜑 → ( Rel 𝐵 ∧ Rel dom 𝐵 ) )

Proof

Step Hyp Ref Expression
1 oppfrcl.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
2 oppfrcl.2 ⊢ Rel 𝑅
3 oppfrcl.3 ⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4 oppfrcl2.4 ⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
5 4 fveq2d ⊢ ( 𝜑 → ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
6 df-ov ⊢ ( 𝐴 oppFunc 𝐵 ) = ( oppFunc ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7 5 3 6 3eqtr4g ⊢ ( 𝜑 → 𝐺 = ( 𝐴 oppFunc 𝐵 ) )
8 1 2 3 4 oppfrcl2 ⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
9 oppfvalg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 oppFunc 𝐵 ) = if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) )
10 8 9 syl ⊢ ( 𝜑 → ( 𝐴 oppFunc 𝐵 ) = if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) )
11 7 10 eqtrd ⊢ ( 𝜑 → 𝐺 = if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) )
12 1 2 oppfrcllem ⊢ ( 𝜑 → 𝐺 ≠ ∅ )
13 11 12 eqnetrrd ⊢ ( 𝜑 → if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) ≠ ∅ )
14 iffalse ⊢ ( ¬ ( Rel 𝐵 ∧ Rel dom 𝐵 ) → if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) = ∅ )
15 14 necon1ai ⊢ ( if ( ( Rel 𝐵 ∧ Rel dom 𝐵 ) , ⟨ 𝐴 , tpos 𝐵 ⟩ , ∅ ) ≠ ∅ → ( Rel 𝐵 ∧ Rel dom 𝐵 ) )
16 13 15 syl ⊢ ( 𝜑 → ( Rel 𝐵 ∧ Rel dom 𝐵 ) )