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		df-oppf	⊢ oppFunc = ( 𝑓 ∈ V , 𝑔 ∈ V ↦ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) )
10		opex	⊢ ⟨ 𝑓 , tpos 𝑔 ⟩ ∈ V
11		0ex	⊢ ∅ ∈ V
12	10 11	ifex	⊢ if ( ( Rel 𝑔 ∧ Rel dom 𝑔 ) , ⟨ 𝑓 , tpos 𝑔 ⟩ , ∅ ) ∈ V
13	9 12	dmmpo	⊢ dom oppFunc = ( V × V )
14	8 13	eleqtrdi	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )