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 → A B = C D ↔ A = C ∧ B = D

Proof

Step Hyp Ref Expression
1 preq12bg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ V ∧ D ∈ V → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
2 1 adantlr ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D ∧ C ∈ V ∧ D ∈ V → A B = C D ↔ 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 → A B = C D ↔ A = C ∧ B = D
14 13 expcom ⊢ C ∈ V ∧ D ∈ V → A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D ↔ 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 → A B ≠ C D
21 19 20 sylan ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D ∧ ¬ C ∈ V → A B ≠ C D
22 21 ancoms ⊢ ¬ C ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B ≠ C D
23 eqneqall ⊢ A B = C D → A B ≠ C D → A = C ∧ B = D
24 22 23 syl5com ⊢ ¬ C ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D → A = C ∧ B = D
25 prneprprc ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ D ∈ V → A B ≠ D C
26 19 25 sylan ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D ∧ ¬ D ∈ V → A B ≠ D C
27 26 ancoms ⊢ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B ≠ D C
28 prcom ⊢ C D = D C
29 28 eqeq2i ⊢ A B = C D ↔ A B = D C
30 eqneqall ⊢ A B = D C → A B ≠ D C → A = C ∧ B = D
31 29 30 sylbi ⊢ A B = C D → A B ≠ D C → A = C ∧ B = D
32 27 31 syl5com ⊢ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D → A = C ∧ B = D
33 24 32 jaoian ⊢ ¬ C ∈ V ∨ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D → A = C ∧ B = D
34 preq12 ⊢ A = C ∧ B = D → A B = C D
35 33 34 impbid1 ⊢ ¬ C ∈ V ∨ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D ↔ A = C ∧ B = D
36 35 ex ⊢ ¬ C ∈ V ∨ ¬ D ∈ V → A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D ↔ A = C ∧ B = D
37 15 36 sylbi ⊢ ¬ C ∈ V ∧ D ∈ V → A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D ↔ A = C ∧ B = D
38 14 37 pm2.61i ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ A ≠ D → A B = C D ↔ A = C ∧ B = D