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