# Metamath Proof Explorer

## Theorem pr2ne

Description: If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010)

Ref Expression
Assertion pr2ne ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\left\{{A},{B}\right\}\approx {2}_{𝑜}↔{A}\ne {B}\right)$

### Proof

Step Hyp Ref Expression
1 preq2 ${⊢}{B}={A}\to \left\{{A},{B}\right\}=\left\{{A},{A}\right\}$
2 1 eqcoms ${⊢}{A}={B}\to \left\{{A},{B}\right\}=\left\{{A},{A}\right\}$
3 enpr1g ${⊢}{A}\in {C}\to \left\{{A},{A}\right\}\approx {1}_{𝑜}$
4 entr ${⊢}\left(\left\{{A},{B}\right\}\approx \left\{{A},{A}\right\}\wedge \left\{{A},{A}\right\}\approx {1}_{𝑜}\right)\to \left\{{A},{B}\right\}\approx {1}_{𝑜}$
5 1sdom2 ${⊢}{1}_{𝑜}\prec {2}_{𝑜}$
6 sdomnen ${⊢}{1}_{𝑜}\prec {2}_{𝑜}\to ¬{1}_{𝑜}\approx {2}_{𝑜}$
7 5 6 ax-mp ${⊢}¬{1}_{𝑜}\approx {2}_{𝑜}$
8 ensym ${⊢}\left\{{A},{B}\right\}\approx {1}_{𝑜}\to {1}_{𝑜}\approx \left\{{A},{B}\right\}$
9 entr ${⊢}\left({1}_{𝑜}\approx \left\{{A},{B}\right\}\wedge \left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\to {1}_{𝑜}\approx {2}_{𝑜}$
10 9 ex ${⊢}{1}_{𝑜}\approx \left\{{A},{B}\right\}\to \left(\left\{{A},{B}\right\}\approx {2}_{𝑜}\to {1}_{𝑜}\approx {2}_{𝑜}\right)$
11 8 10 syl ${⊢}\left\{{A},{B}\right\}\approx {1}_{𝑜}\to \left(\left\{{A},{B}\right\}\approx {2}_{𝑜}\to {1}_{𝑜}\approx {2}_{𝑜}\right)$
12 7 11 mtoi ${⊢}\left\{{A},{B}\right\}\approx {1}_{𝑜}\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}$
13 12 a1d ${⊢}\left\{{A},{B}\right\}\approx {1}_{𝑜}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)$
14 4 13 syl ${⊢}\left(\left\{{A},{B}\right\}\approx \left\{{A},{A}\right\}\wedge \left\{{A},{A}\right\}\approx {1}_{𝑜}\right)\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)$
15 14 ex ${⊢}\left\{{A},{B}\right\}\approx \left\{{A},{A}\right\}\to \left(\left\{{A},{A}\right\}\approx {1}_{𝑜}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\right)$
16 prex ${⊢}\left\{{A},{B}\right\}\in \mathrm{V}$
17 eqeng ${⊢}\left\{{A},{B}\right\}\in \mathrm{V}\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left\{{A},{B}\right\}\approx \left\{{A},{A}\right\}\right)$
18 16 17 ax-mp ${⊢}\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left\{{A},{B}\right\}\approx \left\{{A},{A}\right\}$
19 15 18 syl11 ${⊢}\left\{{A},{A}\right\}\approx {1}_{𝑜}\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\right)$
20 19 a1dd ${⊢}\left\{{A},{A}\right\}\approx {1}_{𝑜}\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left({B}\in {D}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\right)\right)$
21 3 20 syl ${⊢}{A}\in {C}\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left({B}\in {D}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\right)\right)$
22 21 com23 ${⊢}{A}\in {C}\to \left({B}\in {D}\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\right)\right)$
23 22 imp ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to \left(\left({A}\in {C}\wedge {B}\in {D}\right)\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)\right)$
24 23 pm2.43a ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\left\{{A},{B}\right\}=\left\{{A},{A}\right\}\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)$
25 2 24 syl5 ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left({A}={B}\to ¬\left\{{A},{B}\right\}\approx {2}_{𝑜}\right)$
26 25 necon2ad ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\left\{{A},{B}\right\}\approx {2}_{𝑜}\to {A}\ne {B}\right)$
27 pr2nelem ${⊢}\left({A}\in {C}\wedge {B}\in {D}\wedge {A}\ne {B}\right)\to \left\{{A},{B}\right\}\approx {2}_{𝑜}$
28 27 3expia ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left({A}\ne {B}\to \left\{{A},{B}\right\}\approx {2}_{𝑜}\right)$
29 26 28 impbid ${⊢}\left({A}\in {C}\wedge {B}\in {D}\right)\to \left(\left\{{A},{B}\right\}\approx {2}_{𝑜}↔{A}\ne {B}\right)$