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		df-oppf	Could not format oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) : No typesetting found for |- oppFunc = ( f e. _V , g e. _V |-> if ( ( Rel g /\ Rel dom g ) , <. f , tpos g >. , (/) ) ) with typecode |-
10		opex	$$⊢⟨f,tposg⟩\in \mathrm{V}$$
11		0ex	$$⊢\varnothing \in \mathrm{V}$$
12	10 11	ifex	$$⊢if\left(\left(\mathrm{Rel}g\wedge \mathrm{Rel}\mathrm{dom}g\right),⟨f,tposg⟩,\varnothing \right)\in \mathrm{V}$$
13	9 12	dmmpo	Could not format dom oppFunc = ( _V X. _V ) : No typesetting found for |- dom oppFunc = ( _V X. _V ) with typecode |-
14	8 13	eleqtrdi	$$⊢\phi \to F\in \left(\mathrm{V}\times \mathrm{V}\right)$$