Theorem oppfrcllem

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

	Ref	Expression
Hypotheses	oppfrcl.1	$$⊢\phi \to G\in R$$
	oppfrcl.2	$$⊢\mathrm{Rel}R$$
Assertion	oppfrcllem	$$⊢\phi \to G\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	$$⊢\phi \to G\in R$$
2		oppfrcl.2	$$⊢\mathrm{Rel}R$$
3		0nelrel0	$$⊢\mathrm{Rel}R\to \neg \varnothing \in R$$
4	2 3	ax-mp	$$⊢\neg \varnothing \in R$$
5		nelne2	$$⊢\left(G\in R\wedge \neg \varnothing \in R\right)\to G\ne \varnothing$$
6	1 4 5	sylancl	$$⊢\phi \to G\ne \varnothing$$