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