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	⊢ ( 𝜑 → 𝐵 = { 𝐴 } )
Assertion	oppcmndclem	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ≠ 𝑌 → 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcmndclem.1	⊢ ( 𝜑 → 𝐵 = { 𝐴 } )
2		df-ne	⊢ ( 𝑋 ≠ 𝑌 ↔ ¬ 𝑋 = 𝑌 )
3		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
4		eqeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 = 𝑦 ↔ 𝑋 = 𝑌 ) )
5		mosn	⊢ ( 𝐵 = { 𝐴 } → ∃* 𝑥 𝑥 ∈ 𝐵 )
6	1 5	syl	⊢ ( 𝜑 → ∃* 𝑥 𝑥 ∈ 𝐵 )
7		moel	⊢ ( ∃* 𝑥 𝑥 ∈ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
8	6 7	sylib	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
9	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 𝑥 = 𝑦 )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 ∈ 𝐵 )
11		simprr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑌 ∈ 𝐵 )
12	3 4 9 10 11	rspc2dv	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → 𝑋 = 𝑌 )
13	12	pm2.24d	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ¬ 𝑋 = 𝑌 → 𝜓 ) )
14	2 13	biimtrid	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ≠ 𝑌 → 𝜓 ) )