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

Metamath Proof Explorer

Theorem oppfrcllem

Description: Lemma for oppfrcl . (Contributed by Zhi Wang, 14-Nov-2025)

Ref Expression
Hypotheses oppfrcl.1 ⊢ φ → G ∈ R
oppfrcl.2 ⊢ Rel ⁡ R
Assertion oppfrcllem ⊢ φ → G ≠ ∅

Proof

Step Hyp Ref Expression
1 oppfrcl.1 ⊢ φ → G ∈ R
2 oppfrcl.2 ⊢ Rel ⁡ R
3 0nelrel0 ⊢ Rel ⁡ R → ¬ ∅ ∈ R
4 2 3 ax-mp ⊢ ¬ ∅ ∈ R
5 nelne2 ⊢ G ∈ R ∧ ¬ ∅ ∈ R → G ≠ ∅
6 1 4 5 sylancl ⊢ φ → G ≠ ∅