Metamath Proof Explorer


Theorem preleqg

Description: Equality of two unordered pairs when one member of each pair contains the other member. Closed form of preleq . (Contributed by AV, 15-Jun-2022)

Ref Expression
Assertion preleqg ( ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 elneq ( 𝐴𝐵𝐴𝐵 )
2 1 3ad2ant1 ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → 𝐴𝐵 )
3 preq12nebg ( ( 𝐴𝐵𝐵𝑉𝐴𝐵 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) ) )
4 2 3 syld3an3 ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) ) )
5 eleq12 ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( 𝐴𝐵𝐷𝐶 ) )
6 elnotel ( 𝐷𝐶 → ¬ 𝐶𝐷 )
7 6 pm2.21d ( 𝐷𝐶 → ( 𝐶𝐷 → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
8 5 7 syl6bi ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( 𝐴𝐵 → ( 𝐶𝐷 → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) )
9 8 com3l ( 𝐴𝐵 → ( 𝐶𝐷 → ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) )
10 9 a1d ( 𝐴𝐵 → ( 𝐵𝑉 → ( 𝐶𝐷 → ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) ) )
11 10 3imp ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
12 11 com12 ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
13 12 jao1i ( ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) → ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
14 13 com12 ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → ( ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
15 4 14 sylbid ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
16 15 imp ( ( ( 𝐴𝐵𝐵𝑉𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )