Metamath Proof Explorer


Theorem fodomfi

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodom 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)

Ref Expression
Assertion fodomfi
|- ( ( A e. Fin /\ F : A -onto-> B ) -> B ~<_ A )

Proof

Step Hyp Ref Expression
1 foima
 |-  ( F : A -onto-> B -> ( F " A ) = B )
2 1 adantl
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) = B )
3 imaeq2
 |-  ( x = (/) -> ( F " x ) = ( F " (/) ) )
4 ima0
 |-  ( F " (/) ) = (/)
5 3 4 eqtrdi
 |-  ( x = (/) -> ( F " x ) = (/) )
6 id
 |-  ( x = (/) -> x = (/) )
7 5 6 breq12d
 |-  ( x = (/) -> ( ( F " x ) ~<_ x <-> (/) ~<_ (/) ) )
8 7 imbi2d
 |-  ( x = (/) -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> (/) ~<_ (/) ) ) )
9 imaeq2
 |-  ( x = y -> ( F " x ) = ( F " y ) )
10 id
 |-  ( x = y -> x = y )
11 9 10 breq12d
 |-  ( x = y -> ( ( F " x ) ~<_ x <-> ( F " y ) ~<_ y ) )
12 11 imbi2d
 |-  ( x = y -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " y ) ~<_ y ) ) )
13 imaeq2
 |-  ( x = ( y u. { z } ) -> ( F " x ) = ( F " ( y u. { z } ) ) )
14 id
 |-  ( x = ( y u. { z } ) -> x = ( y u. { z } ) )
15 13 14 breq12d
 |-  ( x = ( y u. { z } ) -> ( ( F " x ) ~<_ x <-> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) )
16 15 imbi2d
 |-  ( x = ( y u. { z } ) -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
17 imaeq2
 |-  ( x = A -> ( F " x ) = ( F " A ) )
18 id
 |-  ( x = A -> x = A )
19 17 18 breq12d
 |-  ( x = A -> ( ( F " x ) ~<_ x <-> ( F " A ) ~<_ A ) )
20 19 imbi2d
 |-  ( x = A -> ( ( F Fn A -> ( F " x ) ~<_ x ) <-> ( F Fn A -> ( F " A ) ~<_ A ) ) )
21 0ex
 |-  (/) e. _V
22 21 0dom
 |-  (/) ~<_ (/)
23 22 a1i
 |-  ( F Fn A -> (/) ~<_ (/) )
24 fnfun
 |-  ( F Fn A -> Fun F )
25 24 ad2antrl
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> Fun F )
26 funressn
 |-  ( Fun F -> ( F |` { z } ) C_ { <. z , ( F ` z ) >. } )
27 rnss
 |-  ( ( F |` { z } ) C_ { <. z , ( F ` z ) >. } -> ran ( F |` { z } ) C_ ran { <. z , ( F ` z ) >. } )
28 25 26 27 3syl
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ran ( F |` { z } ) C_ ran { <. z , ( F ` z ) >. } )
29 df-ima
 |-  ( F " { z } ) = ran ( F |` { z } )
30 vex
 |-  z e. _V
31 30 rnsnop
 |-  ran { <. z , ( F ` z ) >. } = { ( F ` z ) }
32 31 eqcomi
 |-  { ( F ` z ) } = ran { <. z , ( F ` z ) >. }
33 28 29 32 3sstr4g
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) C_ { ( F ` z ) } )
34 snex
 |-  { ( F ` z ) } e. _V
35 ssexg
 |-  ( ( ( F " { z } ) C_ { ( F ` z ) } /\ { ( F ` z ) } e. _V ) -> ( F " { z } ) e. _V )
36 33 34 35 sylancl
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) e. _V )
37 fvi
 |-  ( ( F " { z } ) e. _V -> ( _I ` ( F " { z } ) ) = ( F " { z } ) )
38 36 37 syl
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) = ( F " { z } ) )
39 38 uneq2d
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) = ( ( F " y ) u. ( F " { z } ) ) )
40 imaundi
 |-  ( F " ( y u. { z } ) ) = ( ( F " y ) u. ( F " { z } ) )
41 39 40 eqtr4di
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) = ( F " ( y u. { z } ) ) )
42 simprr
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " y ) ~<_ y )
43 ssdomg
 |-  ( { ( F ` z ) } e. _V -> ( ( F " { z } ) C_ { ( F ` z ) } -> ( F " { z } ) ~<_ { ( F ` z ) } ) )
44 34 33 43 mpsyl
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { ( F ` z ) } )
45 fvex
 |-  ( F ` z ) e. _V
46 45 ensn1
 |-  { ( F ` z ) } ~~ 1o
47 30 ensn1
 |-  { z } ~~ 1o
48 46 47 entr4i
 |-  { ( F ` z ) } ~~ { z }
49 domentr
 |-  ( ( ( F " { z } ) ~<_ { ( F ` z ) } /\ { ( F ` z ) } ~~ { z } ) -> ( F " { z } ) ~<_ { z } )
50 44 48 49 sylancl
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { z } )
51 38 50 eqbrtrd
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) ~<_ { z } )
52 simplr
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> -. z e. y )
53 disjsn
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
54 52 53 sylibr
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( y i^i { z } ) = (/) )
55 undom
 |-  ( ( ( ( F " y ) ~<_ y /\ ( _I ` ( F " { z } ) ) ~<_ { z } ) /\ ( y i^i { z } ) = (/) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) )
56 42 51 54 55 syl21anc
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) )
57 41 56 eqbrtrrd
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) )
58 57 exp32
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( F Fn A -> ( ( F " y ) ~<_ y -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
59 58 a2d
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( F Fn A -> ( F " y ) ~<_ y ) -> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
60 8 12 16 20 23 59 findcard2s
 |-  ( A e. Fin -> ( F Fn A -> ( F " A ) ~<_ A ) )
61 fofn
 |-  ( F : A -onto-> B -> F Fn A )
62 60 61 impel
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) ~<_ A )
63 2 62 eqbrtrrd
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> B ~<_ A )