Metamath Proof Explorer

Theorem preq12nebg

Description: Equality relationship for two proper unordered pairs. (Contributed by AV, 12-Jun-2022)

Ref Expression
Assertion preq12nebg ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C

Proof

Step Hyp Ref Expression
1 3simpa ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ V ∧ B ∈ W
2 1 anim1i ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ C ∈ V ∧ D ∈ V → A ∈ V ∧ B ∈ W ∧ C ∈ V ∧ D ∈ V
3 2 ancoms ⊢ C ∈ V ∧ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A ∈ V ∧ B ∈ W ∧ C ∈ V ∧ D ∈ V
4 preq12bg ⊢ A ∈ V ∧ B ∈ W ∧ C ∈ V ∧ D ∈ V → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
5 3 4 syl ⊢ C ∈ V ∧ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
6 5 ex ⊢ C ∈ V ∧ D ∈ V → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
7 ianor ⊢ ¬ C ∈ V ∧ D ∈ V ↔ ¬ C ∈ V ∨ ¬ D ∈ V
8 prneprprc ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ C ∈ V → A B ≠ C D
9 8 ancoms ⊢ ¬ C ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ C D
10 eqneqall ⊢ A B = C D → A B ≠ C D → A = C ∧ B = D ∨ A = D ∧ B = C
11 9 10 syl5com ⊢ ¬ C ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D → A = C ∧ B = D ∨ A = D ∧ B = C
12 prneprprc ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B ∧ ¬ D ∈ V → A B ≠ D C
13 12 ancoms ⊢ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B ≠ D C
14 prcom ⊢ C D = D C
15 14 eqeq2i ⊢ A B = C D ↔ A B = D C
16 eqneqall ⊢ A B = D C → A B ≠ D C → A = C ∧ B = D ∨ A = D ∧ B = C
17 15 16 sylbi ⊢ A B = C D → A B ≠ D C → A = C ∧ B = D ∨ A = D ∧ B = C
18 13 17 syl5com ⊢ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D → A = C ∧ B = D ∨ A = D ∧ B = C
19 11 18 jaoian ⊢ ¬ C ∈ V ∨ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D → A = C ∧ B = D ∨ A = D ∧ B = C
20 preq12 ⊢ A = C ∧ B = D → A B = C D
21 preq12 ⊢ A = D ∧ B = C → A B = D C
22 prcom ⊢ D C = C D
23 21 22 eqtrdi ⊢ A = D ∧ B = C → A B = C D
24 20 23 jaoi ⊢ A = C ∧ B = D ∨ A = D ∧ B = C → A B = C D
25 19 24 impbid1 ⊢ ¬ C ∈ V ∨ ¬ D ∈ V ∧ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
26 25 ex ⊢ ¬ C ∈ V ∨ ¬ D ∈ V → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
27 7 26 sylbi ⊢ ¬ C ∈ V ∧ D ∈ V → A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
28 6 27 pm2.61i ⊢ A ∈ V ∧ B ∈ W ∧ A ≠ B → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C