Theorem pr2ne

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

	Ref	Expression
Assertion	pr2ne	|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )

Proof

Step	Hyp	Ref	Expression
1		preq2	|- ( B = A -> { A , B } = { A , A } )
2	1	eqcoms	|- ( A = B -> { A , B } = { A , A } )
3		enpr1g	|- ( A e. C -> { A , A } ~~ 1o )
4		entr	|- ( ( { A , B } ~~ { A , A } /\ { A , A } ~~ 1o ) -> { A , B } ~~ 1o )
5		1sdom2	|- 1o ~< 2o
6		sdomnen	|- ( 1o ~< 2o -> -. 1o ~~ 2o )
7	5 6	ax-mp	|- -. 1o ~~ 2o
8		ensym	|- ( { A , B } ~~ 1o -> 1o ~~ { A , B } )
9		entr	|- ( ( 1o ~~ { A , B } /\ { A , B } ~~ 2o ) -> 1o ~~ 2o )
10	9	ex	|- ( 1o ~~ { A , B } -> ( { A , B } ~~ 2o -> 1o ~~ 2o ) )
11	8 10	syl	|- ( { A , B } ~~ 1o -> ( { A , B } ~~ 2o -> 1o ~~ 2o ) )
12	7 11	mtoi	|- ( { A , B } ~~ 1o -> -. { A , B } ~~ 2o )
13	12	a1d	|- ( { A , B } ~~ 1o -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) )
14	4 13	syl	|- ( ( { A , B } ~~ { A , A } /\ { A , A } ~~ 1o ) -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) )
15	14	ex	|- ( { A , B } ~~ { A , A } -> ( { A , A } ~~ 1o -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) ) )
16		prex	|- { A , B } e. _V
17		eqeng	|- ( { A , B } e. _V -> ( { A , B } = { A , A } -> { A , B } ~~ { A , A } ) )
18	16 17	ax-mp	|- ( { A , B } = { A , A } -> { A , B } ~~ { A , A } )
19	15 18	syl11	|- ( { A , A } ~~ 1o -> ( { A , B } = { A , A } -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) ) )
20	19	a1dd	|- ( { A , A } ~~ 1o -> ( { A , B } = { A , A } -> ( B e. D -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) ) ) )
21	3 20	syl	|- ( A e. C -> ( { A , B } = { A , A } -> ( B e. D -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) ) ) )
22	21	com23	|- ( A e. C -> ( B e. D -> ( { A , B } = { A , A } -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) ) ) )
23	22	imp	|- ( ( A e. C /\ B e. D ) -> ( { A , B } = { A , A } -> ( ( A e. C /\ B e. D ) -> -. { A , B } ~~ 2o ) ) )
24	23	pm2.43a	|- ( ( A e. C /\ B e. D ) -> ( { A , B } = { A , A } -> -. { A , B } ~~ 2o ) )
25	2 24	syl5	|- ( ( A e. C /\ B e. D ) -> ( A = B -> -. { A , B } ~~ 2o ) )
26	25	necon2ad	|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o -> A =/= B ) )
27		pr2nelem	|- ( ( A e. C /\ B e. D /\ A =/= B ) -> { A , B } ~~ 2o )
28	27	3expia	|- ( ( A e. C /\ B e. D ) -> ( A =/= B -> { A , B } ~~ 2o ) )
29	26 28	impbid	|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )