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 ⊢ 𝐹 = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ 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 ‘ 𝐴 ) )