# Metamath Proof Explorer

## Theorem opthprneg

Description: An unordered pair has the ordered pair property (compare opth ) under certain conditions. Variant of opthpr in closed form. (Contributed by AV, 13-Jun-2022)

Ref Expression
Assertion opthprneg ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)$

### Proof

Step Hyp Ref Expression
1 preq12bg ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)\right)$
2 1 adantlr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\wedge \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)\right)$
3 idd ${⊢}{A}\ne {D}\to \left(\left({A}={C}\wedge {B}={D}\right)\to \left({A}={C}\wedge {B}={D}\right)\right)$
4 df-ne ${⊢}{A}\ne {D}↔¬{A}={D}$
5 pm2.21 ${⊢}¬{A}={D}\to \left({A}={D}\to \left({B}={C}\to \left({A}={C}\wedge {B}={D}\right)\right)\right)$
6 4 5 sylbi ${⊢}{A}\ne {D}\to \left({A}={D}\to \left({B}={C}\to \left({A}={C}\wedge {B}={D}\right)\right)\right)$
7 6 impd ${⊢}{A}\ne {D}\to \left(\left({A}={D}\wedge {B}={C}\right)\to \left({A}={C}\wedge {B}={D}\right)\right)$
8 3 7 jaod ${⊢}{A}\ne {D}\to \left(\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)\to \left({A}={C}\wedge {B}={D}\right)\right)$
9 orc ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)$
10 8 9 impbid1 ${⊢}{A}\ne {D}\to \left(\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)↔\left({A}={C}\wedge {B}={D}\right)\right)$
11 10 adantl ${⊢}\left({A}\ne {B}\wedge {A}\ne {D}\right)\to \left(\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)↔\left({A}={C}\wedge {B}={D}\right)\right)$
12 11 ad2antlr ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\wedge \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\right)\to \left(\left(\left({A}={C}\wedge {B}={D}\right)\vee \left({A}={D}\wedge {B}={C}\right)\right)↔\left({A}={C}\wedge {B}={D}\right)\right)$
13 2 12 bitrd ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\wedge \left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)$
14 13 expcom ${⊢}\left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\to \left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)\right)$
15 ianor ${⊢}¬\left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)↔\left(¬{C}\in \mathrm{V}\vee ¬{D}\in \mathrm{V}\right)$
16 simpl ${⊢}\left({A}\ne {B}\wedge {A}\ne {D}\right)\to {A}\ne {B}$
17 16 anim2i ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge {A}\ne {B}\right)$
18 df-3an ${⊢}\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)↔\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge {A}\ne {B}\right)$
19 17 18 sylibr ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)$
20 prneprprc ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\wedge ¬{C}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}$
21 19 20 sylan ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\wedge ¬{C}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}$
22 21 ancoms ${⊢}\left(¬{C}\in \mathrm{V}\wedge \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\right)\to \left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}$
23 eqneqall ${⊢}\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left(\left\{{A},{B}\right\}\ne \left\{{C},{D}\right\}\to \left({A}={C}\wedge {B}={D}\right)\right)$
24 22 23 syl5com ${⊢}\left(¬{C}\in \mathrm{V}\wedge \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left({A}={C}\wedge {B}={D}\right)\right)$
25 prneprprc ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\wedge {A}\ne {B}\right)\wedge ¬{D}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{D},{C}\right\}$
26 19 25 sylan ${⊢}\left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\wedge ¬{D}\in \mathrm{V}\right)\to \left\{{A},{B}\right\}\ne \left\{{D},{C}\right\}$
27 26 ancoms ${⊢}\left(¬{D}\in \mathrm{V}\wedge \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\right)\to \left\{{A},{B}\right\}\ne \left\{{D},{C}\right\}$
28 prcom ${⊢}\left\{{C},{D}\right\}=\left\{{D},{C}\right\}$
29 28 eqeq2i ${⊢}\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left\{{A},{B}\right\}=\left\{{D},{C}\right\}$
30 eqneqall ${⊢}\left\{{A},{B}\right\}=\left\{{D},{C}\right\}\to \left(\left\{{A},{B}\right\}\ne \left\{{D},{C}\right\}\to \left({A}={C}\wedge {B}={D}\right)\right)$
31 29 30 sylbi ${⊢}\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left(\left\{{A},{B}\right\}\ne \left\{{D},{C}\right\}\to \left({A}={C}\wedge {B}={D}\right)\right)$
32 27 31 syl5com ${⊢}\left(¬{D}\in \mathrm{V}\wedge \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left({A}={C}\wedge {B}={D}\right)\right)$
33 24 32 jaoian ${⊢}\left(\left(¬{C}\in \mathrm{V}\vee ¬{D}\in \mathrm{V}\right)\wedge \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}\to \left({A}={C}\wedge {B}={D}\right)\right)$
34 preq12 ${⊢}\left({A}={C}\wedge {B}={D}\right)\to \left\{{A},{B}\right\}=\left\{{C},{D}\right\}$
35 33 34 impbid1 ${⊢}\left(\left(¬{C}\in \mathrm{V}\vee ¬{D}\in \mathrm{V}\right)\wedge \left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)$
36 35 ex ${⊢}\left(¬{C}\in \mathrm{V}\vee ¬{D}\in \mathrm{V}\right)\to \left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)\right)$
37 15 36 sylbi ${⊢}¬\left({C}\in \mathrm{V}\wedge {D}\in \mathrm{V}\right)\to \left(\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)\right)$
38 14 37 pm2.61i ${⊢}\left(\left({A}\in {V}\wedge {B}\in {W}\right)\wedge \left({A}\ne {B}\wedge {A}\ne {D}\right)\right)\to \left(\left\{{A},{B}\right\}=\left\{{C},{D}\right\}↔\left({A}={C}\wedge {B}={D}\right)\right)$