This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppfrcl2

Description: If an opposite functor of a class is a functor, then the two components of the original class must be sets. (Contributed by Zhi Wang, 14-Nov-2025)

		Ref	Expression
	Hypotheses	oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
		oppfrcl.2	⊢ Rel 𝑅
		oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
		oppfrcl2.4	⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
	Assertion	oppfrcl2	⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
2		oppfrcl.2	⊢ Rel 𝑅
3		oppfrcl.3	⊢ 𝐺 = ( oppFunc ‘ 𝐹 )
4		oppfrcl2.4	⊢ ( 𝜑 → 𝐹 = ⟨ 𝐴 , 𝐵 ⟩ )
5	1 2 3	oppfrcl	⊢ ( 𝜑 → 𝐹 ∈ ( V × V ) )
6	4 5	eqeltrrd	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
7		0nelxp	⊢ ¬ ∅ ∈ ( V × V )
8		nelne2	⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ∧ ¬ ∅ ∈ ( V × V ) ) → ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ )
9	6 7 8	sylancl	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ )
10		opprc	⊢ ( ¬ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ⟨ 𝐴 , 𝐵 ⟩ = ∅ )
11	10	necon1ai	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ≠ ∅ → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
12	9 11	syl	⊢ ( 𝜑 → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )