Metamath Proof Explorer

Theorem birthdaylem1

Description: Lemma for birthday . (Contributed by Mario Carneiro, 17-Apr-2015)

Ref Expression
Hypotheses birthday.s 
|- S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }
birthday.t 
|- T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }
Assertion birthdaylem1 
|- ( T C_ S /\ S e. Fin /\ ( N e. NN -> S =/= (/) ) )

Proof

Step Hyp Ref Expression
1 birthday.s 
 |-  S = { f | f : ( 1 ... K ) --> ( 1 ... N ) }
2 birthday.t 
 |-  T = { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) }
3 f1f 
 |-  ( f : ( 1 ... K ) -1-1-> ( 1 ... N ) -> f : ( 1 ... K ) --> ( 1 ... N ) )
4 3 ss2abi 
 |-  { f | f : ( 1 ... K ) -1-1-> ( 1 ... N ) } C_ { f | f : ( 1 ... K ) --> ( 1 ... N ) }
5 4 2 1 3sstr4i 
 |-  T C_ S
6 fzfi 
 |-  ( 1 ... N ) e. Fin
7 fzfi 
 |-  ( 1 ... K ) e. Fin
8 mapvalg 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( 1 ... K ) e. Fin ) -> ( ( 1 ... N ) ^m ( 1 ... K ) ) = { f | f : ( 1 ... K ) --> ( 1 ... N ) } )
9 6 7 8 mp2an 
 |-  ( ( 1 ... N ) ^m ( 1 ... K ) ) = { f | f : ( 1 ... K ) --> ( 1 ... N ) }
10 1 9 eqtr4i 
 |-  S = ( ( 1 ... N ) ^m ( 1 ... K ) )
11 mapfi 
 |-  ( ( ( 1 ... N ) e. Fin /\ ( 1 ... K ) e. Fin ) -> ( ( 1 ... N ) ^m ( 1 ... K ) ) e. Fin )
12 6 7 11 mp2an 
 |-  ( ( 1 ... N ) ^m ( 1 ... K ) ) e. Fin
13 10 12 eqeltri 
 |-  S e. Fin
14 elfz1end 
 |-  ( N e. NN <-> N e. ( 1 ... N ) )
15 ne0i 
 |-  ( N e. ( 1 ... N ) -> ( 1 ... N ) =/= (/) )
16 14 15 sylbi 
 |-  ( N e. NN -> ( 1 ... N ) =/= (/) )
17 10 eqeq1i 
 |-  ( S = (/) <-> ( ( 1 ... N ) ^m ( 1 ... K ) ) = (/) )
18 ovex 
 |-  ( 1 ... N ) e. _V
19 ovex 
 |-  ( 1 ... K ) e. _V
20 18 19 map0 
 |-  ( ( ( 1 ... N ) ^m ( 1 ... K ) ) = (/) <-> ( ( 1 ... N ) = (/) /\ ( 1 ... K ) =/= (/) ) )
21 20 simplbi 
 |-  ( ( ( 1 ... N ) ^m ( 1 ... K ) ) = (/) -> ( 1 ... N ) = (/) )
22 17 21 sylbi 
 |-  ( S = (/) -> ( 1 ... N ) = (/) )
23 22 necon3i 
 |-  ( ( 1 ... N ) =/= (/) -> S =/= (/) )
24 16 23 syl 
 |-  ( N e. NN -> S =/= (/) )
25 5 13 24 3pm3.2i 
 |-  ( T C_ S /\ S e. Fin /\ ( N e. NN -> S =/= (/) ) )