This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )