This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )