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	⊢ ( 𝜑 → 𝐺 ≠ ∅ )