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 ⊢A∈V∧B∈W∧A≠B∧A≠D→AB=CD↔A=C∧B=D

Proof

Step Hyp Ref Expression
1 preq12bg ⊢A∈V∧B∈W∧C∈V∧D∈V→AB=CD↔A=C∧B=D∨A=D∧B=C
2 1 adantlr ⊢A∈V∧B∈W∧A≠B∧A≠D∧C∈V∧D∈V→AB=CD↔A=C∧B=D∨A=D∧B=C
3 idd ⊢A≠D→A=C∧B=D→A=C∧B=D
4 df-ne ⊢A≠D↔¬A=D
5 pm2.21 ⊢¬A=D→A=D→B=C→A=C∧B=D
6 4 5 sylbi ⊢A≠D→A=D→B=C→A=C∧B=D
7 6 impd ⊢A≠D→A=D∧B=C→A=C∧B=D
8 3 7 jaod ⊢A≠D→A=C∧B=D∨A=D∧B=C→A=C∧B=D
9 orc ⊢A=C∧B=D→A=C∧B=D∨A=D∧B=C
10 8 9 impbid1 ⊢A≠D→A=C∧B=D∨A=D∧B=C↔A=C∧B=D
11 10 adantl ⊢A≠B∧A≠D→A=C∧B=D∨A=D∧B=C↔A=C∧B=D
12 11 ad2antlr ⊢A∈V∧B∈W∧A≠B∧A≠D∧C∈V∧D∈V→A=C∧B=D∨A=D∧B=C↔A=C∧B=D
13 2 12 bitrd ⊢A∈V∧B∈W∧A≠B∧A≠D∧C∈V∧D∈V→AB=CD↔A=C∧B=D
14 13 expcom ⊢C∈V∧D∈V→A∈V∧B∈W∧A≠B∧A≠D→AB=CD↔A=C∧B=D
15 ianor ⊢¬C∈V∧D∈V↔¬C∈V∨¬D∈V
16 simpl ⊢A≠B∧A≠D→A≠B
17 16 anim2i ⊢A∈V∧B∈W∧A≠B∧A≠D→A∈V∧B∈W∧A≠B
18 df-3an ⊢A∈V∧B∈W∧A≠B↔A∈V∧B∈W∧A≠B
19 17 18 sylibr ⊢A∈V∧B∈W∧A≠B∧A≠D→A∈V∧B∈W∧A≠B
20 prneprprc ⊢A∈V∧B∈W∧A≠B∧¬C∈V→AB≠CD
21 19 20 sylan ⊢A∈V∧B∈W∧A≠B∧A≠D∧¬C∈V→AB≠CD
22 21 ancoms ⊢¬C∈V∧A∈V∧B∈W∧A≠B∧A≠D→AB≠CD
23 eqneqall ⊢AB=CD→AB≠CD→A=C∧B=D
24 22 23 syl5com ⊢¬C∈V∧A∈V∧B∈W∧A≠B∧A≠D→AB=CD→A=C∧B=D
25 prneprprc ⊢A∈V∧B∈W∧A≠B∧¬D∈V→AB≠DC
26 19 25 sylan ⊢A∈V∧B∈W∧A≠B∧A≠D∧¬D∈V→AB≠DC
27 26 ancoms ⊢¬D∈V∧A∈V∧B∈W∧A≠B∧A≠D→AB≠DC
28 prcom ⊢CD=DC
29 28 eqeq2i ⊢AB=CD↔AB=DC
30 eqneqall ⊢AB=DC→AB≠DC→A=C∧B=D
31 29 30 sylbi ⊢AB=CD→AB≠DC→A=C∧B=D
32 27 31 syl5com ⊢¬D∈V∧A∈V∧B∈W∧A≠B∧A≠D→AB=CD→A=C∧B=D
33 24 32 jaoian ⊢¬C∈V∨¬D∈V∧A∈V∧B∈W∧A≠B∧A≠D→AB=CD→A=C∧B=D
34 preq12 ⊢A=C∧B=D→AB=CD
35 33 34 impbid1 ⊢¬C∈V∨¬D∈V∧A∈V∧B∈W∧A≠B∧A≠D→AB=CD↔A=C∧B=D
36 35 ex ⊢¬C∈V∨¬D∈V→A∈V∧B∈W∧A≠B∧A≠D→AB=CD↔A=C∧B=D
37 15 36 sylbi ⊢¬C∈V∧D∈V→A∈V∧B∈W∧A≠B∧A≠D→AB=CD↔A=C∧B=D
38 14 37 pm2.61i ⊢A∈V∧B∈W∧A≠B∧A≠D→AB=CD↔A=C∧B=D