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