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∖∅⟶ontofi⁡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→FFn𝒫A∩Fin∖∅
7 5 6 mp1i ⊢A∈V→FFn𝒫A∩Fin∖∅
8 dffn4 ⊢FFn𝒫A∩Fin∖∅↔F:𝒫A∩Fin∖∅⟶ontoran⁡F
9 7 8 sylib ⊢A∈V→F:𝒫A∩Fin∖∅⟶ontoran⁡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∖∅⟶ontofi⁡A↔F:𝒫A∩Fin∖∅⟶ontoran⁡F
16 14 15 syl ⊢A∈V→F:𝒫A∩Fin∖∅⟶ontofi⁡A↔F:𝒫A∩Fin∖∅⟶ontoran⁡F
17 9 16 mpbird ⊢A∈V→F:𝒫A∩Fin∖∅⟶ontofi⁡A