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	$⊢ φ \to G \in R$
		oppfrcl.2	$⊢ Rel R$
		oppfrcl.3	No typesetting found for \|- G = ( oppFunc ` F ) with typecode \|-
		oppfrcl2.4	$⊢ φ \to F = ⟨A, B⟩$
	Assertion	oppfrcl2	$⊢ φ \to (A \in V \land B \in V)$

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	$⊢ φ \to G \in R$
2		oppfrcl.2	$⊢ Rel R$
3		oppfrcl.3	Could not format G = ( oppFunc ` F ) : No typesetting found for \|- G = ( oppFunc ` F ) with typecode \|-
4		oppfrcl2.4	$⊢ φ \to F = ⟨A, B⟩$
5	1 2 3	oppfrcl	$⊢ φ \to F \in (V \times V)$
6	4 5	eqeltrrd	$⊢ φ \to ⟨A, B⟩ \in (V \times V)$
7		0nelxp	$⊢ \neg \emptyset \in (V \times V)$
8		nelne2	$⊢ (⟨A, B⟩ \in (V \times V) \land \neg \emptyset \in (V \times V)) \to ⟨A, B⟩ \neq \emptyset$
9	6 7 8	sylancl	$⊢ φ \to ⟨A, B⟩ \neq \emptyset$
10		opprc	$⊢ \neg (A \in V \land B \in V) \to ⟨A, B⟩ = \emptyset$
11	10	necon1ai	$⊢ ⟨A, B⟩ \neq \emptyset \to (A \in V \land B \in V)$
12	9 11	syl	$⊢ φ \to (A \in V \land B \in V)$