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 𝐹 = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ 𝑦 )
Assertion fifo ( 𝐴𝑉𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fifo.1 𝐹 = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ 𝑦 )
2 eldifsni ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ≠ ∅ )
3 intex ( 𝑦 ≠ ∅ ↔ 𝑦 ∈ V )
4 2 3 sylib ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) → 𝑦 ∈ V )
5 4 rgen 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑦 ∈ V
6 1 fnmpt ( ∀ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑦 ∈ V → 𝐹 Fn ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
7 5 6 mp1i ( 𝐴𝑉𝐹 Fn ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
8 dffn4 ( 𝐹 Fn ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↔ 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 )
9 7 8 sylib ( 𝐴𝑉𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 )
10 elfi2 ( 𝐴𝑉 → ( 𝑥 ∈ ( fi ‘ 𝐴 ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑥 = 𝑦 ) )
11 1 elrnmpt ( 𝑥 ∈ V → ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑥 = 𝑦 ) )
12 11 elv ( 𝑥 ∈ ran 𝐹 ↔ ∃ 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) 𝑥 = 𝑦 )
13 10 12 bitr4di ( 𝐴𝑉 → ( 𝑥 ∈ ( fi ‘ 𝐴 ) ↔ 𝑥 ∈ ran 𝐹 ) )
14 13 eqrdv ( 𝐴𝑉 → ( fi ‘ 𝐴 ) = ran 𝐹 )
15 foeq3 ( ( fi ‘ 𝐴 ) = ran 𝐹 → ( 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) ↔ 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 ) )
16 14 15 syl ( 𝐴𝑉 → ( 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) ↔ 𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ran 𝐹 ) )
17 9 16 mpbird ( 𝐴𝑉𝐹 : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )