Metamath Proof Explorer


Theorem fifo

Description: Describe a surjection from nonempty finite sets to finite intersections. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Hypothesis fifo.1
|- F = ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y )
Assertion fifo
|- ( A e. V -> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )

Proof

Step Hyp Ref Expression
1 fifo.1
 |-  F = ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y )
2 eldifsni
 |-  ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) -> y =/= (/) )
3 intex
 |-  ( y =/= (/) <-> |^| y e. _V )
4 2 3 sylib
 |-  ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) -> |^| y e. _V )
5 4 rgen
 |-  A. y e. ( ( ~P A i^i Fin ) \ { (/) } ) |^| y e. _V
6 1 fnmpt
 |-  ( A. y e. ( ( ~P A i^i Fin ) \ { (/) } ) |^| y e. _V -> F Fn ( ( ~P A i^i Fin ) \ { (/) } ) )
7 5 6 mp1i
 |-  ( A e. V -> F Fn ( ( ~P A i^i Fin ) \ { (/) } ) )
8 dffn4
 |-  ( F Fn ( ( ~P A i^i Fin ) \ { (/) } ) <-> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F )
9 7 8 sylib
 |-  ( A e. V -> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F )
10 elfi2
 |-  ( A e. V -> ( x e. ( fi ` A ) <-> E. y e. ( ( ~P A i^i Fin ) \ { (/) } ) x = |^| y ) )
11 1 elrnmpt
 |-  ( x e. _V -> ( x e. ran F <-> E. y e. ( ( ~P A i^i Fin ) \ { (/) } ) x = |^| y ) )
12 11 elv
 |-  ( x e. ran F <-> E. y e. ( ( ~P A i^i Fin ) \ { (/) } ) x = |^| y )
13 10 12 bitr4di
 |-  ( A e. V -> ( x e. ( fi ` A ) <-> x e. ran F ) )
14 13 eqrdv
 |-  ( A e. V -> ( fi ` A ) = ran F )
15 foeq3
 |-  ( ( fi ` A ) = ran F -> ( F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) <-> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F ) )
16 14 15 syl
 |-  ( A e. V -> ( F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) <-> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ran F ) )
17 9 16 mpbird
 |-  ( A e. V -> F : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )