Metamath Proof Explorer

Theorem 1sdom

Description: A set that strictly dominates ordinal 1 has at least 2 different members. (Closely related to 2dom .) (Contributed by Mario Carneiro, 12-Jan-2013)

Ref Expression
Assertion 1sdom 
|- ( A e. V -> ( 1o ~< A <-> E. x e. A E. y e. A -. x = y ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( a = A -> ( 1o ~< a <-> 1o ~< A ) )
2 rexeq 
 |-  ( a = A -> ( E. y e. a -. x = y <-> E. y e. A -. x = y ) )
3 2 rexeqbi1dv 
 |-  ( a = A -> ( E. x e. a E. y e. a -. x = y <-> E. x e. A E. y e. A -. x = y ) )
4 1onn 
 |-  1o e. _om
5 sucdom 
 |-  ( 1o e. _om -> ( 1o ~< a <-> suc 1o ~<_ a ) )
6 4 5 ax-mp 
 |-  ( 1o ~< a <-> suc 1o ~<_ a )
7 df-2o 
 |-  2o = suc 1o
8 7 breq1i 
 |-  ( 2o ~<_ a <-> suc 1o ~<_ a )
9 2dom 
 |-  ( 2o ~<_ a -> E. x e. a E. y e. a -. x = y )
10 df2o3 
 |-  2o = { (/) , 1o }
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 0ex 
 |-  (/) e. _V
14 1oex 
 |-  1o e. _V
15 11 12 13 14 funpr 
 |-  ( x =/= y -> Fun { <. x , (/) >. , <. y , 1o >. } )
16 df-ne 
 |-  ( x =/= y <-> -. x = y )
17 1n0 
 |-  1o =/= (/)
18 17 necomi 
 |-  (/) =/= 1o
19 13 14 11 12 fpr 
 |-  ( (/) =/= 1o -> { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } --> { x , y } )
20 18 19 ax-mp 
 |-  { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } --> { x , y }
21 df-f1 
 |-  ( { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> { x , y } <-> ( { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } --> { x , y } /\ Fun `' { <. (/) , x >. , <. 1o , y >. } ) )
22 20 21 mpbiran 
 |-  ( { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> { x , y } <-> Fun `' { <. (/) , x >. , <. 1o , y >. } )
23 13 11 cnvsn 
 |-  `' { <. (/) , x >. } = { <. x , (/) >. }
24 14 12 cnvsn 
 |-  `' { <. 1o , y >. } = { <. y , 1o >. }
25 23 24 uneq12i 
 |-  ( `' { <. (/) , x >. } u. `' { <. 1o , y >. } ) = ( { <. x , (/) >. } u. { <. y , 1o >. } )
26 df-pr 
 |-  { <. (/) , x >. , <. 1o , y >. } = ( { <. (/) , x >. } u. { <. 1o , y >. } )
27 26 cnveqi 
 |-  `' { <. (/) , x >. , <. 1o , y >. } = `' ( { <. (/) , x >. } u. { <. 1o , y >. } )
28 cnvun 
 |-  `' ( { <. (/) , x >. } u. { <. 1o , y >. } ) = ( `' { <. (/) , x >. } u. `' { <. 1o , y >. } )
29 27 28 eqtri 
 |-  `' { <. (/) , x >. , <. 1o , y >. } = ( `' { <. (/) , x >. } u. `' { <. 1o , y >. } )
30 df-pr 
 |-  { <. x , (/) >. , <. y , 1o >. } = ( { <. x , (/) >. } u. { <. y , 1o >. } )
31 25 29 30 3eqtr4i 
 |-  `' { <. (/) , x >. , <. 1o , y >. } = { <. x , (/) >. , <. y , 1o >. }
32 31 funeqi 
 |-  ( Fun `' { <. (/) , x >. , <. 1o , y >. } <-> Fun { <. x , (/) >. , <. y , 1o >. } )
33 22 32 bitr2i 
 |-  ( Fun { <. x , (/) >. , <. y , 1o >. } <-> { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> { x , y } )
34 15 16 33 3imtr3i 
 |-  ( -. x = y -> { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> { x , y } )
35 prssi 
 |-  ( ( x e. a /\ y e. a ) -> { x , y } C_ a )
36 f1ss 
 |-  ( ( { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> { x , y } /\ { x , y } C_ a ) -> { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> a )
37 34 35 36 syl2an 
 |-  ( ( -. x = y /\ ( x e. a /\ y e. a ) ) -> { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> a )
38 prex 
 |-  { <. (/) , x >. , <. 1o , y >. } e. _V
39 f1eq1 
 |-  ( f = { <. (/) , x >. , <. 1o , y >. } -> ( f : { (/) , 1o } -1-1-> a <-> { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> a ) )
40 38 39 spcev 
 |-  ( { <. (/) , x >. , <. 1o , y >. } : { (/) , 1o } -1-1-> a -> E. f f : { (/) , 1o } -1-1-> a )
41 37 40 syl 
 |-  ( ( -. x = y /\ ( x e. a /\ y e. a ) ) -> E. f f : { (/) , 1o } -1-1-> a )
42 vex 
 |-  a e. _V
43 42 brdom 
 |-  ( { (/) , 1o } ~<_ a <-> E. f f : { (/) , 1o } -1-1-> a )
44 41 43 sylibr 
 |-  ( ( -. x = y /\ ( x e. a /\ y e. a ) ) -> { (/) , 1o } ~<_ a )
45 44 expcom 
 |-  ( ( x e. a /\ y e. a ) -> ( -. x = y -> { (/) , 1o } ~<_ a ) )
46 45 rexlimivv 
 |-  ( E. x e. a E. y e. a -. x = y -> { (/) , 1o } ~<_ a )
47 10 46 eqbrtrid 
 |-  ( E. x e. a E. y e. a -. x = y -> 2o ~<_ a )
48 9 47 impbii 
 |-  ( 2o ~<_ a <-> E. x e. a E. y e. a -. x = y )
49 6 8 48 3bitr2i 
 |-  ( 1o ~< a <-> E. x e. a E. y e. a -. x = y )
50 1 3 49 vtoclbg 
 |-  ( A e. V -> ( 1o ~< A <-> E. x e. A E. y e. A -. x = y ) )