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