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	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
	oppfrcl.2	⊢ Rel 𝑅
	oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
Assertion	oppfrcl	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
2		oppfrcl.2	⊢ Rel 𝑅
3		oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4	1 2	oppfrcllem	⊢ ( 𝜑 → 𝐺 ≠ ∅ )
5		ndmfv	⊢ ( ¬ 𝐹 ∈ dom oppFunc → ( oppFunc ‘ 𝐹 ) = ∅ )
6	3 5	eqtrid	⊢ ( ¬ 𝐹 ∈ dom oppFunc → 𝐺 = ∅ )
7	6	necon1ai	⊢ ( 𝐺 ≠ ∅ → 𝐹 ∈ dom oppFunc )
8	4 7	syl	⊢ ( 𝜑 → 𝐹 ∈ dom oppFunc )
9		oppffn	⊢ oppFunc Fn ( V × V )
10	9	fndmi	⊢ dom oppFunc = ( V × V )
11	8 10	eleqtrdi	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )