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 𝒫 A Fin y
Assertion fifo A V F : 𝒫 A Fin onto fi A

Proof

Step Hyp Ref Expression
1 fifo.1 F = y 𝒫 A Fin y
2 eldifsni y 𝒫 A Fin y
3 intex y y V
4 2 3 sylib y 𝒫 A Fin y V
5 4 rgen y 𝒫 A Fin y V
6 1 fnmpt y 𝒫 A Fin y V F Fn 𝒫 A Fin
7 5 6 mp1i A V F Fn 𝒫 A Fin
8 dffn4 F Fn 𝒫 A Fin F : 𝒫 A Fin onto ran F
9 7 8 sylib A V F : 𝒫 A Fin onto ran F
10 elfi2 A V x fi A y 𝒫 A Fin x = y
11 1 elrnmpt x V x ran F y 𝒫 A Fin x = y
12 11 elv x ran F y 𝒫 A Fin x = y
13 10 12 bitr4di A V x fi A x ran F
14 13 eqrdv A V fi A = ran F
15 foeq3 fi A = ran F F : 𝒫 A Fin onto fi A F : 𝒫 A Fin onto ran F
16 14 15 syl A V F : 𝒫 A Fin onto fi A F : 𝒫 A Fin onto ran F
17 9 16 mpbird A V F : 𝒫 A Fin onto fi A