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

Metamath Proof Explorer

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 )