Theorem pr2ne

Description: If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010)

	Ref	Expression
Assertion	pr2ne	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ≈ 2o ↔ 𝐴 ≠ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		preq2	⊢ ( 𝐵 = 𝐴 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } )
2	1	eqcoms	⊢ ( 𝐴 = 𝐵 → { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } )
3		enpr1g	⊢ ( 𝐴 ∈ 𝐶 → { 𝐴 , 𝐴 } ≈ 1o )
4		entr	⊢ ( ( { 𝐴 , 𝐵 } ≈ { 𝐴 , 𝐴 } ∧ { 𝐴 , 𝐴 } ≈ 1o ) → { 𝐴 , 𝐵 } ≈ 1o )
5		1sdom2	⊢ 1o ≺ 2o
6		sdomnen	⊢ ( 1o ≺ 2o → ¬ 1o ≈ 2o )
7	5 6	ax-mp	⊢ ¬ 1o ≈ 2o
8		ensym	⊢ ( { 𝐴 , 𝐵 } ≈ 1o → 1o ≈ { 𝐴 , 𝐵 } )
9		entr	⊢ ( ( 1o ≈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } ≈ 2o ) → 1o ≈ 2o )
10	9	ex	⊢ ( 1o ≈ { 𝐴 , 𝐵 } → ( { 𝐴 , 𝐵 } ≈ 2o → 1o ≈ 2o ) )
11	8 10	syl	⊢ ( { 𝐴 , 𝐵 } ≈ 1o → ( { 𝐴 , 𝐵 } ≈ 2o → 1o ≈ 2o ) )
12	7 11	mtoi	⊢ ( { 𝐴 , 𝐵 } ≈ 1o → ¬ { 𝐴 , 𝐵 } ≈ 2o )
13	12	a1d	⊢ ( { 𝐴 , 𝐵 } ≈ 1o → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) )
14	4 13	syl	⊢ ( ( { 𝐴 , 𝐵 } ≈ { 𝐴 , 𝐴 } ∧ { 𝐴 , 𝐴 } ≈ 1o ) → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) )
15	14	ex	⊢ ( { 𝐴 , 𝐵 } ≈ { 𝐴 , 𝐴 } → ( { 𝐴 , 𝐴 } ≈ 1o → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) ) )
16		prex	⊢ { 𝐴 , 𝐵 } ∈ V
17		eqeng	⊢ ( { 𝐴 , 𝐵 } ∈ V → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → { 𝐴 , 𝐵 } ≈ { 𝐴 , 𝐴 } ) )
18	16 17	ax-mp	⊢ ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → { 𝐴 , 𝐵 } ≈ { 𝐴 , 𝐴 } )
19	15 18	syl11	⊢ ( { 𝐴 , 𝐴 } ≈ 1o → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) ) )
20	19	a1dd	⊢ ( { 𝐴 , 𝐴 } ≈ 1o → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → ( 𝐵 ∈ 𝐷 → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) ) ) )
21	3 20	syl	⊢ ( 𝐴 ∈ 𝐶 → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → ( 𝐵 ∈ 𝐷 → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) ) ) )
22	21	com23	⊢ ( 𝐴 ∈ 𝐶 → ( 𝐵 ∈ 𝐷 → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) ) ) )
23	22	imp	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ¬ { 𝐴 , 𝐵 } ≈ 2o ) ) )
24	23	pm2.43a	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } = { 𝐴 , 𝐴 } → ¬ { 𝐴 , 𝐵 } ≈ 2o ) )
25	2 24	syl5	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 = 𝐵 → ¬ { 𝐴 , 𝐵 } ≈ 2o ) )
26	25	necon2ad	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ≈ 2o → 𝐴 ≠ 𝐵 ) )
27		pr2nelem	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵 ) → { 𝐴 , 𝐵 } ≈ 2o )
28	27	3expia	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 ≠ 𝐵 → { 𝐴 , 𝐵 } ≈ 2o ) )
29	26 28	impbid	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( { 𝐴 , 𝐵 } ≈ 2o ↔ 𝐴 ≠ 𝐵 ) )