| 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 =/= (/) ) ) |