Theorem prdom2

Description: An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011)

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

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { A } = { A , A }
2		ensn1g	|- ( A e. C -> { A } ~~ 1o )
3		endom	|- ( { A } ~~ 1o -> { A } ~<_ 1o )
4		1sdom2	|- 1o ~< 2o
5		domsdomtr	|- ( ( { A } ~<_ 1o /\ 1o ~< 2o ) -> { A } ~< 2o )
6		sdomdom	|- ( { A } ~< 2o -> { A } ~<_ 2o )
7	5 6	syl	|- ( ( { A } ~<_ 1o /\ 1o ~< 2o ) -> { A } ~<_ 2o )
8	3 4 7	sylancl	|- ( { A } ~~ 1o -> { A } ~<_ 2o )
9	2 8	syl	|- ( A e. C -> { A } ~<_ 2o )
10	1 9	eqbrtrrid	|- ( A e. C -> { A , A } ~<_ 2o )
11		preq2	|- ( B = A -> { A , B } = { A , A } )
12	11	breq1d	|- ( B = A -> ( { A , B } ~<_ 2o <-> { A , A } ~<_ 2o ) )
13	10 12	imbitrrid	|- ( B = A -> ( A e. C -> { A , B } ~<_ 2o ) )
14	13	eqcoms	|- ( A = B -> ( A e. C -> { A , B } ~<_ 2o ) )
15	14	adantrd	|- ( A = B -> ( ( A e. C /\ B e. D ) -> { A , B } ~<_ 2o ) )
16		pr2ne	|- ( ( A e. C /\ B e. D ) -> ( { A , B } ~~ 2o <-> A =/= B ) )
17	16	biimprd	|- ( ( A e. C /\ B e. D ) -> ( A =/= B -> { A , B } ~~ 2o ) )
18		endom	|- ( { A , B } ~~ 2o -> { A , B } ~<_ 2o )
19	17 18	syl6com	|- ( A =/= B -> ( ( A e. C /\ B e. D ) -> { A , B } ~<_ 2o ) )
20	15 19	pm2.61ine	|- ( ( A e. C /\ B e. D ) -> { A , B } ~<_ 2o )