This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem preq12nebg

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

Ref Expression
Assertion preq12nebg ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷 ∧ 𝐵 = 𝐶 ) ) ) )

Proof

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