Theorem oppcmndclem

Description: Lemma for oppcmndc . Everything is true for two distinct elements in a singleton or an empty set (since it is impossible). Note that if this theorem and oppcendc are in -. x = y form, then both proofs should be one step shorter. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypothesis	oppcmndclem.1	|- ( ph -> B = { A } )
Assertion	oppcmndclem	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X =/= Y -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		oppcmndclem.1	|- ( ph -> B = { A } )
2		df-ne	|- ( X =/= Y <-> -. X = Y )
3		eqeq1	|- ( x = X -> ( x = y <-> X = y ) )
4		eqeq2	|- ( y = Y -> ( X = y <-> X = Y ) )
5		mosn	|- ( B = { A } -> E* x x e. B )
6	1 5	syl	|- ( ph -> E* x x e. B )
7		moel	|- ( E* x x e. B <-> A. x e. B A. y e. B x = y )
8	6 7	sylib	|- ( ph -> A. x e. B A. y e. B x = y )
9	8	adantr	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> A. x e. B A. y e. B x = y )
10		simprl	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X e. B )
11		simprr	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> Y e. B )
12	3 4 9 10 11	rspc2dv	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> X = Y )
13	12	pm2.24d	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( -. X = Y -> ps ) )
14	2 13	biimtrid	|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( X =/= Y -> ps ) )