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 )