Metamath Proof Explorer

Theorem 2dom

Description: A set that dominates ordinal 2 has at least 2 different members. (Contributed by NM, 25-Jul-2004)

Ref Expression
Assertion 2dom 
|- ( 2o ~<_ A -> E. x e. A E. y e. A -. x = y )

Proof

Step Hyp Ref Expression
1 df2o2 
 |-  2o = { (/) , { (/) } }
2 1 breq1i 
 |-  ( 2o ~<_ A <-> { (/) , { (/) } } ~<_ A )
3 brdomi 
 |-  ( { (/) , { (/) } } ~<_ A -> E. f f : { (/) , { (/) } } -1-1-> A )
4 2 3 sylbi 
 |-  ( 2o ~<_ A -> E. f f : { (/) , { (/) } } -1-1-> A )
5 f1f 
 |-  ( f : { (/) , { (/) } } -1-1-> A -> f : { (/) , { (/) } } --> A )
6 0ex 
 |-  (/) e. _V
7 6 prid1 
 |-  (/) e. { (/) , { (/) } }
8 ffvelcdm 
 |-  ( ( f : { (/) , { (/) } } --> A /\ (/) e. { (/) , { (/) } } ) -> ( f ` (/) ) e. A )
9 5 7 8 sylancl 
 |-  ( f : { (/) , { (/) } } -1-1-> A -> ( f ` (/) ) e. A )
10 snex 
 |-  { (/) } e. _V
11 10 prid2 
 |-  { (/) } e. { (/) , { (/) } }
12 ffvelcdm 
 |-  ( ( f : { (/) , { (/) } } --> A /\ { (/) } e. { (/) , { (/) } } ) -> ( f ` { (/) } ) e. A )
13 5 11 12 sylancl 
 |-  ( f : { (/) , { (/) } } -1-1-> A -> ( f ` { (/) } ) e. A )
14 0nep0 
 |-  (/) =/= { (/) }
15 14 neii 
 |-  -. (/) = { (/) }
16 f1fveq 
 |-  ( ( f : { (/) , { (/) } } -1-1-> A /\ ( (/) e. { (/) , { (/) } } /\ { (/) } e. { (/) , { (/) } } ) ) -> ( ( f ` (/) ) = ( f ` { (/) } ) <-> (/) = { (/) } ) )
17 7 11 16 mpanr12 
 |-  ( f : { (/) , { (/) } } -1-1-> A -> ( ( f ` (/) ) = ( f ` { (/) } ) <-> (/) = { (/) } ) )
18 15 17 mtbiri 
 |-  ( f : { (/) , { (/) } } -1-1-> A -> -. ( f ` (/) ) = ( f ` { (/) } ) )
19 eqeq1 
 |-  ( x = ( f ` (/) ) -> ( x = y <-> ( f ` (/) ) = y ) )
20 19 notbid 
 |-  ( x = ( f ` (/) ) -> ( -. x = y <-> -. ( f ` (/) ) = y ) )
21 eqeq2 
 |-  ( y = ( f ` { (/) } ) -> ( ( f ` (/) ) = y <-> ( f ` (/) ) = ( f ` { (/) } ) ) )
22 21 notbid 
 |-  ( y = ( f ` { (/) } ) -> ( -. ( f ` (/) ) = y <-> -. ( f ` (/) ) = ( f ` { (/) } ) ) )
23 20 22 rspc2ev 
 |-  ( ( ( f ` (/) ) e. A /\ ( f ` { (/) } ) e. A /\ -. ( f ` (/) ) = ( f ` { (/) } ) ) -> E. x e. A E. y e. A -. x = y )
24 9 13 18 23 syl3anc 
 |-  ( f : { (/) , { (/) } } -1-1-> A -> E. x e. A E. y e. A -. x = y )
25 24 exlimiv 
 |-  ( E. f f : { (/) , { (/) } } -1-1-> A -> E. x e. A E. y e. A -. x = y )
26 4 25 syl 
 |-  ( 2o ~<_ A -> E. x e. A E. y e. A -. x = y )