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