MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fodomfi Structured version   Visualization version   Unicode version

Theorem fodomfi 7881
Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 8983 for arbitrary sets, this theorem does not require the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006.) (Proof shortened by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
fodomfi  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  B  ~<_  A )

Proof of Theorem fodomfi
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 foima 5825 . . 3  |-  ( F : A -onto-> B  -> 
( F " A
)  =  B )
21adantl 472 . 2  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  ( F " A )  =  B )
3 fofn 5822 . . . 4  |-  ( F : A -onto-> B  ->  F  Fn  A )
4 imaeq2 5186 . . . . . . . 8  |-  ( x  =  (/)  ->  ( F
" x )  =  ( F " (/) ) )
5 ima0 5205 . . . . . . . 8  |-  ( F
" (/) )  =  (/)
64, 5syl6eq 2512 . . . . . . 7  |-  ( x  =  (/)  ->  ( F
" x )  =  (/) )
7 id 22 . . . . . . 7  |-  ( x  =  (/)  ->  x  =  (/) )
86, 7breq12d 4431 . . . . . 6  |-  ( x  =  (/)  ->  ( ( F " x )  ~<_  x  <->  (/)  ~<_  (/) ) )
98imbi2d 322 . . . . 5  |-  ( x  =  (/)  ->  ( ( F  Fn  A  -> 
( F " x
)  ~<_  x )  <->  ( F  Fn  A  ->  (/)  ~<_  (/) ) ) )
10 imaeq2 5186 . . . . . . 7  |-  ( x  =  y  ->  ( F " x )  =  ( F " y
) )
11 id 22 . . . . . . 7  |-  ( x  =  y  ->  x  =  y )
1210, 11breq12d 4431 . . . . . 6  |-  ( x  =  y  ->  (
( F " x
)  ~<_  x  <->  ( F " y )  ~<_  y ) )
1312imbi2d 322 . . . . 5  |-  ( x  =  y  ->  (
( F  Fn  A  ->  ( F " x
)  ~<_  x )  <->  ( F  Fn  A  ->  ( F
" y )  ~<_  y ) ) )
14 imaeq2 5186 . . . . . . 7  |-  ( x  =  ( y  u. 
{ z } )  ->  ( F "
x )  =  ( F " ( y  u.  { z } ) ) )
15 id 22 . . . . . . 7  |-  ( x  =  ( y  u. 
{ z } )  ->  x  =  ( y  u.  { z } ) )
1614, 15breq12d 4431 . . . . . 6  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( F
" x )  ~<_  x  <-> 
( F " (
y  u.  { z } ) )  ~<_  ( y  u.  { z } ) ) )
1716imbi2d 322 . . . . 5  |-  ( x  =  ( y  u. 
{ z } )  ->  ( ( F  Fn  A  ->  ( F " x )  ~<_  x )  <->  ( F  Fn  A  ->  ( F "
( y  u.  {
z } ) )  ~<_  ( y  u.  {
z } ) ) ) )
18 imaeq2 5186 . . . . . . 7  |-  ( x  =  A  ->  ( F " x )  =  ( F " A
) )
19 id 22 . . . . . . 7  |-  ( x  =  A  ->  x  =  A )
2018, 19breq12d 4431 . . . . . 6  |-  ( x  =  A  ->  (
( F " x
)  ~<_  x  <->  ( F " A )  ~<_  A ) )
2120imbi2d 322 . . . . 5  |-  ( x  =  A  ->  (
( F  Fn  A  ->  ( F " x
)  ~<_  x )  <->  ( F  Fn  A  ->  ( F
" A )  ~<_  A ) ) )
22 0ex 4551 . . . . . . 7  |-  (/)  e.  _V
23220dom 7733 . . . . . 6  |-  (/)  ~<_  (/)
2423a1i 11 . . . . 5  |-  ( F  Fn  A  ->  (/)  ~<_  (/) )
25 fnfun 5699 . . . . . . . . . . . . . . 15  |-  ( F  Fn  A  ->  Fun  F )
2625ad2antrl 739 . . . . . . . . . . . . . 14  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  Fun  F )
27 funressn 6106 . . . . . . . . . . . . . 14  |-  ( Fun 
F  ->  ( F  |` 
{ z } ) 
C_  { <. z ,  ( F `  z ) >. } )
28 rnss 5085 . . . . . . . . . . . . . 14  |-  ( ( F  |`  { z } )  C_  { <. z ,  ( F `  z ) >. }  ->  ran  ( F  |`  { z } )  C_  ran  {
<. z ,  ( F `
 z ) >. } )
2926, 27, 283syl 18 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ran  ( F  |`  { z } )  C_  ran  {
<. z ,  ( F `
 z ) >. } )
30 df-ima 4869 . . . . . . . . . . . . 13  |-  ( F
" { z } )  =  ran  ( F  |`  { z } )
31 vex 3060 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
3231rnsnop 5340 . . . . . . . . . . . . . 14  |-  ran  { <. z ,  ( F `
 z ) >. }  =  { ( F `  z ) }
3332eqcomi 2471 . . . . . . . . . . . . 13  |-  { ( F `  z ) }  =  ran  { <. z ,  ( F `
 z ) >. }
3429, 30, 333sstr4g 3485 . . . . . . . . . . . 12  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ( F " { z } )  C_  { ( F `  z ) } )
35 snex 4658 . . . . . . . . . . . 12  |-  { ( F `  z ) }  e.  _V
36 ssexg 4565 . . . . . . . . . . . 12  |-  ( ( ( F " {
z } )  C_  { ( F `  z
) }  /\  {
( F `  z
) }  e.  _V )  ->  ( F " { z } )  e.  _V )
3734, 35, 36sylancl 673 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ( F " { z } )  e.  _V )
38 fvi 5950 . . . . . . . . . . 11  |-  ( ( F " { z } )  e.  _V  ->  (  _I  `  ( F " { z } ) )  =  ( F " { z } ) )
3937, 38syl 17 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  (  _I  `  ( F " { z } ) )  =  ( F
" { z } ) )
4039uneq2d 3600 . . . . . . . . 9  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  (
( F " y
)  u.  (  _I 
`  ( F " { z } ) ) )  =  ( ( F " y
)  u.  ( F
" { z } ) ) )
41 imaundi 5270 . . . . . . . . 9  |-  ( F
" ( y  u. 
{ z } ) )  =  ( ( F " y )  u.  ( F " { z } ) )
4240, 41syl6eqr 2514 . . . . . . . 8  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  (
( F " y
)  u.  (  _I 
`  ( F " { z } ) ) )  =  ( F " ( y  u.  { z } ) ) )
43 simprr 771 . . . . . . . . 9  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ( F " y )  ~<_  y )
44 ssdomg 7646 . . . . . . . . . . . 12  |-  ( { ( F `  z
) }  e.  _V  ->  ( ( F " { z } ) 
C_  { ( F `
 z ) }  ->  ( F " { z } )  ~<_  { ( F `  z ) } ) )
4535, 34, 44mpsyl 65 . . . . . . . . . . 11  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ( F " { z } )  ~<_  { ( F `
 z ) } )
46 fvex 5902 . . . . . . . . . . . . 13  |-  ( F `
 z )  e. 
_V
4746ensn1 7664 . . . . . . . . . . . 12  |-  { ( F `  z ) }  ~~  1o
4831ensn1 7664 . . . . . . . . . . . 12  |-  { z }  ~~  1o
4947, 48entr4i 7657 . . . . . . . . . . 11  |-  { ( F `  z ) }  ~~  { z }
50 domentr 7659 . . . . . . . . . . 11  |-  ( ( ( F " {
z } )  ~<_  { ( F `  z
) }  /\  {
( F `  z
) }  ~~  {
z } )  -> 
( F " {
z } )  ~<_  { z } )
5145, 49, 50sylancl 673 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ( F " { z } )  ~<_  { z } )
5239, 51eqbrtrd 4439 . . . . . . . . 9  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  (  _I  `  ( F " { z } ) )  ~<_  { z } )
53 simplr 767 . . . . . . . . . 10  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  -.  z  e.  y )
54 disjsn 4044 . . . . . . . . . 10  |-  ( ( y  i^i  { z } )  =  (/)  <->  -.  z  e.  y )
5553, 54sylibr 217 . . . . . . . . 9  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  (
y  i^i  { z } )  =  (/) )
56 undom 7691 . . . . . . . . 9  |-  ( ( ( ( F "
y )  ~<_  y  /\  (  _I  `  ( F
" { z } ) )  ~<_  { z } )  /\  (
y  i^i  { z } )  =  (/) )  ->  ( ( F
" y )  u.  (  _I  `  ( F " { z } ) ) )  ~<_  ( y  u.  { z } ) )
5743, 52, 55, 56syl21anc 1275 . . . . . . . 8  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  (
( F " y
)  u.  (  _I 
`  ( F " { z } ) ) )  ~<_  ( y  u.  { z } ) )
5842, 57eqbrtrrd 4441 . . . . . . 7  |-  ( ( ( y  e.  Fin  /\ 
-.  z  e.  y )  /\  ( F  Fn  A  /\  ( F " y )  ~<_  y ) )  ->  ( F " ( y  u. 
{ z } ) )  ~<_  ( y  u. 
{ z } ) )
5958exp32 614 . . . . . 6  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( F  Fn  A  ->  ( ( F " y )  ~<_  y  ->  ( F " ( y  u.  {
z } ) )  ~<_  ( y  u.  {
z } ) ) ) )
6059a2d 29 . . . . 5  |-  ( ( y  e.  Fin  /\  -.  z  e.  y
)  ->  ( ( F  Fn  A  ->  ( F " y )  ~<_  y )  ->  ( F  Fn  A  ->  ( F " ( y  u.  { z } ) )  ~<_  ( y  u.  { z } ) ) ) )
619, 13, 17, 21, 24, 60findcard2s 7843 . . . 4  |-  ( A  e.  Fin  ->  ( F  Fn  A  ->  ( F " A )  ~<_  A ) )
623, 61syl5 33 . . 3  |-  ( A  e.  Fin  ->  ( F : A -onto-> B  -> 
( F " A
)  ~<_  A ) )
6362imp 435 . 2  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  ( F " A )  ~<_  A )
642, 63eqbrtrrd 4441 1  |-  ( ( A  e.  Fin  /\  F : A -onto-> B )  ->  B  ~<_  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 375    = wceq 1455    e. wcel 1898   _Vcvv 3057    u. cun 3414    i^i cin 3415    C_ wss 3416   (/)c0 3743   {csn 3980   <.cop 3986   class class class wbr 4418    _I cid 4766   ran crn 4857    |` cres 4858   "cima 4859   Fun wfun 5599    Fn wfn 5600   -onto->wfo 5603   ` cfv 5605   1oc1o 7206    ~~ cen 7597    ~<_ cdom 7598   Fincfn 7600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-br 4419  df-opab 4478  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-om 6725  df-1o 7213  df-er 7394  df-en 7601  df-dom 7602  df-fin 7604
This theorem is referenced by:  fodomfib  7882  fofinf1o  7883  fidomdm  7884  fofi  7891  pwfilem  7899  cmpsub  20470  alexsubALT  21121  phpreu  31975  poimirlem26  32012
  Copyright terms: Public domain W3C validator