Metamath Proof Explorer


Theorem preleqALT

Description: Alternate proof of preleq , not based on preleqg : Equality of two unordered pairs when one member of each pair contains the other member. (Contributed by NM, 16-Oct-1996) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses preleq.b 𝐵 ∈ V
preleqALT.d 𝐷 ∈ V
Assertion preleqALT ( ( ( 𝐴𝐵𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 preleq.b 𝐵 ∈ V
2 preleqALT.d 𝐷 ∈ V
3 1 jctr ( 𝐴𝐵 → ( 𝐴𝐵𝐵 ∈ V ) )
4 2 jctr ( 𝐶𝐷 → ( 𝐶𝐷𝐷 ∈ V ) )
5 preq12bg ( ( ( 𝐴𝐵𝐵 ∈ V ) ∧ ( 𝐶𝐷𝐷 ∈ V ) ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) ) )
6 3 4 5 syl2an ( ( 𝐴𝐵𝐶𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ↔ ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) ) )
7 6 biimpa ( ( ( 𝐴𝐵𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ( 𝐴 = 𝐶𝐵 = 𝐷 ) ∨ ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) )
8 7 ord ( ( ( 𝐴𝐵𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ¬ ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ( 𝐴 = 𝐷𝐵 = 𝐶 ) ) )
9 en2lp ¬ ( 𝐷𝐶𝐶𝐷 )
10 eleq12 ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( 𝐴𝐵𝐷𝐶 ) )
11 10 anbi1d ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ( ( 𝐴𝐵𝐶𝐷 ) ↔ ( 𝐷𝐶𝐶𝐷 ) ) )
12 9 11 mtbiri ( ( 𝐴 = 𝐷𝐵 = 𝐶 ) → ¬ ( 𝐴𝐵𝐶𝐷 ) )
13 8 12 syl6 ( ( ( 𝐴𝐵𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ¬ ( 𝐴 = 𝐶𝐵 = 𝐷 ) → ¬ ( 𝐴𝐵𝐶𝐷 ) ) )
14 13 con4d ( ( ( 𝐴𝐵𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( ( 𝐴𝐵𝐶𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
15 14 ex ( ( 𝐴𝐵𝐶𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( ( 𝐴𝐵𝐶𝐷 ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) ) )
16 15 pm2.43a ( ( 𝐴𝐵𝐶𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } → ( 𝐴 = 𝐶𝐵 = 𝐷 ) ) )
17 16 imp ( ( ( 𝐴𝐵𝐶𝐷 ) ∧ { 𝐴 , 𝐵 } = { 𝐶 , 𝐷 } ) → ( 𝐴 = 𝐶𝐵 = 𝐷 ) )