Theorem oppfrcllem

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

	Ref	Expression
Hypotheses	oppfrcl.1	|- ( ph -> G e. R )
	oppfrcl.2	|- Rel R
Assertion	oppfrcllem	|- ( ph -> G =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		oppfrcl.1	|- ( ph -> G e. R )
2		oppfrcl.2	|- Rel R
3		0nelrel0	|- ( Rel R -> -. (/) e. R )
4	2 3	ax-mp	|- -. (/) e. R
5		nelne2	|- ( ( G e. R /\ -. (/) e. R ) -> G =/= (/) )
6	1 4 5	sylancl	|- ( ph -> G =/= (/) )