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	$$⊢\phi \to G\in R$$
	oppfrcl.2	$$⊢\mathrm{Rel}R$$
	oppfrcl.3	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	oppfrcl2.4	$$⊢\phi \to F=⟨A,B⟩$$
Assertion	oppfrcl3	$$⊢\phi \to \left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	$$⊢\phi \to G\in R$$
2		oppfrcl.2	$$⊢\mathrm{Rel}R$$
3		oppfrcl.3	Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
4		oppfrcl2.4	$$⊢\phi \to 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	$$⊢\phi \to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
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	$$⊢\phi \to G=if\left(\left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right),⟨A,tposB⟩,\varnothing \right)$$
12	1 2	oppfrcllem	$$⊢\phi \to G\ne \varnothing$$
13	11 12	eqnetrrd	$$⊢\phi \to if\left(\left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right),⟨A,tposB⟩,\varnothing \right)\ne \varnothing$$
14		iffalse	$$⊢\neg \left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right)\to if\left(\left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right),⟨A,tposB⟩,\varnothing \right)=\varnothing$$
15	14	necon1ai	$$⊢if\left(\left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right),⟨A,tposB⟩,\varnothing \right)\ne \varnothing \to \left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right)$$
16	13 15	syl	$$⊢\phi \to \left(\mathrm{Rel}B\wedge \mathrm{Rel}\mathrm{dom}B\right)$$