Theorem oppfrcl

Description: If an opposite functor of a class is a functor, then the original class must be an ordered pair. (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 |-
Assertion	oppfrcl	$$⊢\phi \to F\in \left(\mathrm{V}\times \mathrm{V}\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	1 2	oppfrcllem	$$⊢\phi \to G\ne \varnothing$$
5		ndmfv	Could not format ( -. F e. dom oppFunc -> ( oppFunc ` F ) = (/) ) : No typesetting found for |- ( -. F e. dom oppFunc -> ( oppFunc ` F ) = (/) ) with typecode |-
6	3 5	eqtrid	Could not format ( -. F e. dom oppFunc -> G = (/) ) : No typesetting found for |- ( -. F e. dom oppFunc -> G = (/) ) with typecode |-
7	6	necon1ai	Could not format ( G =/= (/) -> F e. dom oppFunc ) : No typesetting found for |- ( G =/= (/) -> F e. dom oppFunc ) with typecode |-
8	4 7	syl	Could not format ( ph -> F e. dom oppFunc ) : No typesetting found for |- ( ph -> F e. dom oppFunc ) with typecode |-
9		oppffn	Could not format oppFunc Fn ( _V X. _V ) : No typesetting found for |- oppFunc Fn ( _V X. _V ) with typecode |-
10	9	fndmi	Could not format dom oppFunc = ( _V X. _V ) : No typesetting found for |- dom oppFunc = ( _V X. _V ) with typecode |-
11	8 10	eleqtrdi	$$⊢\phi \to F\in \left(\mathrm{V}\times \mathrm{V}\right)$$