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 ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐷 ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ) )

Proof

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