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