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 ⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
oppfrcl.2 ⊢ Rel 𝑅
Assertion oppfrcllem ( 𝜑 → 𝐺 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 oppfrcl.1 ⊢ ( 𝜑 → 𝐺 ∈ 𝑅 )
2 oppfrcl.2 ⊢ Rel 𝑅
3 0nelrel0 ⊢ ( Rel 𝑅 → ¬ ∅ ∈ 𝑅 )
4 2 3 ax-mp ⊢ ¬ ∅ ∈ 𝑅
5 nelne2 ⊢ ( ( 𝐺 ∈ 𝑅 ∧ ¬ ∅ ∈ 𝑅 ) → 𝐺 ≠ ∅ )
6 1 4 5 sylancl ⊢ ( 𝜑 → 𝐺 ≠ ∅ )