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

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