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 ⊢ φ → G ∈ R
oppfrcl.2 ⊢ Rel ⁡ R
oppfrcl.3 No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
oppfrcl2.4 ⊢ φ → F = A B
Assertion oppfrcl2 ⊢ φ → A ∈ V ∧ B ∈ V

Proof

Step Hyp Ref Expression
1 oppfrcl.1 ⊢ φ → G ∈ 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 ⊢ φ → F = A B
5 1 2 3 oppfrcl ⊢ φ → F ∈ V × V
6 4 5 eqeltrrd ⊢ φ → A B ∈ V × V
7 0nelxp ⊢ ¬ ∅ ∈ V × V
8 nelne2 ⊢ A B ∈ V × V ∧ ¬ ∅ ∈ V × V → A B ≠ ∅
9 6 7 8 sylancl ⊢ φ → A B ≠ ∅
10 opprc ⊢ ¬ A ∈ V ∧ B ∈ V → A B = ∅
11 10 necon1ai ⊢ A B ≠ ∅ → A ∈ V ∧ B ∈ V
12 9 11 syl ⊢ φ → A ∈ V ∧ B ∈ V