Metamath Proof Explorer

Theorem fodomfi

Description: An onto function implies dominance of domain over range, for finite sets. Unlike fodomg for arbitrary sets, this theorem does not require the Axiom of Replacement nor the Axiom of Power Sets nor the Axiom of Choice for its proof. (Contributed by NM, 23-Mar-2006) (Proof shortened by Mario Carneiro, 16-Nov-2014) Avoid ax-pow . (Revised by BTernaryTau, 20-Jun-2025)

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 snfi 
 |-  { ( F ` z ) } e. Fin
35 ssexg 
 |-  ( ( ( F " { z } ) C_ { ( F ` z ) } /\ { ( F ` z ) } e. Fin ) -> ( 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 ssdomfi 
 |-  ( { ( F ` z ) } e. Fin -> ( ( 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 en2sn 
 |-  ( ( ( F ` z ) e. _V /\ z e. _V ) -> { ( F ` z ) } ~~ { z } )
47 45 30 46 mp2an 
 |-  { ( F ` z ) } ~~ { z }
48 endom 
 |-  ( { ( F ` z ) } ~~ { z } -> { ( F ` z ) } ~<_ { z } )
49 domtrfi 
 |-  ( ( { ( F ` z ) } e. Fin /\ ( F " { z } ) ~<_ { ( F ` z ) } /\ { ( F ` z ) } ~<_ { z } ) -> ( F " { z } ) ~<_ { z } )
50 34 49 mp3an1 
 |-  ( ( ( F " { z } ) ~<_ { ( F ` z ) } /\ { ( F ` z ) } ~<_ { z } ) -> ( F " { z } ) ~<_ { z } )
51 48 50 sylan2 
 |-  ( ( ( F " { z } ) ~<_ { ( F ` z ) } /\ { ( F ` z ) } ~~ { z } ) -> ( F " { z } ) ~<_ { z } )
52 44 47 51 sylancl 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " { z } ) ~<_ { z } )
53 38 52 eqbrtrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( _I ` ( F " { z } ) ) ~<_ { z } )
54 simplr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> -. z e. y )
55 disjsn 
 |-  ( ( y i^i { z } ) = (/) <-> -. z e. y )
56 54 55 sylibr 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( y i^i { z } ) = (/) )
57 undom 
 |-  ( ( ( ( F " y ) ~<_ y /\ ( _I ` ( F " { z } ) ) ~<_ { z } ) /\ ( y i^i { z } ) = (/) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) )
58 42 53 56 57 syl21anc 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( ( F " y ) u. ( _I ` ( F " { z } ) ) ) ~<_ ( y u. { z } ) )
59 41 58 eqbrtrrd 
 |-  ( ( ( y e. Fin /\ -. z e. y ) /\ ( F Fn A /\ ( F " y ) ~<_ y ) ) -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) )
60 59 exp32 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( F Fn A -> ( ( F " y ) ~<_ y -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
61 60 a2d 
 |-  ( ( y e. Fin /\ -. z e. y ) -> ( ( F Fn A -> ( F " y ) ~<_ y ) -> ( F Fn A -> ( F " ( y u. { z } ) ) ~<_ ( y u. { z } ) ) ) )
62 8 12 16 20 23 61 findcard2s 
 |-  ( A e. Fin -> ( F Fn A -> ( F " A ) ~<_ A ) )
63 fofn 
 |-  ( F : A -onto-> B -> F Fn A )
64 62 63 impel 
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> ( F " A ) ~<_ A )
65 2 64 eqbrtrrd 
 |-  ( ( A e. Fin /\ F : A -onto-> B ) -> B ~<_ A )