Metamath Proof Explorer

Theorem intrnfi

Description: Sufficient condition for the intersection of the range of a function to be in the set of finite intersections. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion intrnfi ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ ran ⁡ F ∈ fi ⁡ B

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → F : A ⟶ B
2 1 frnd ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → ran ⁡ F ⊆ B
3 1 fdmd ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → dom ⁡ F = A
4 simpr2 ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ≠ ∅
5 3 4 eqnetrd ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → dom ⁡ F ≠ ∅
6 dm0rn0 ⊢ dom ⁡ F = ∅ ↔ ran ⁡ F = ∅
7 6 necon3bii ⊢ dom ⁡ F ≠ ∅ ↔ ran ⁡ F ≠ ∅
8 5 7 sylib ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → ran ⁡ F ≠ ∅
9 simpr3 ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ∈ Fin
10 1 ffnd ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → F Fn A
11 dffn4 ⊢ F Fn A ↔ F : A ⟶ onto ran ⁡ F
12 10 11 sylib ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → F : A ⟶ onto ran ⁡ F
13 fofi ⊢ A ∈ Fin ∧ F : A ⟶ onto ran ⁡ F → ran ⁡ F ∈ Fin
14 9 12 13 syl2anc ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → ran ⁡ F ∈ Fin
15 2 8 14 3jca ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → ran ⁡ F ⊆ B ∧ ran ⁡ F ≠ ∅ ∧ ran ⁡ F ∈ Fin
16 elfir ⊢ B ∈ V ∧ ran ⁡ F ⊆ B ∧ ran ⁡ F ≠ ∅ ∧ ran ⁡ F ∈ Fin → ⋂ ran ⁡ F ∈ fi ⁡ B
17 15 16 syldan ⊢ B ∈ V ∧ F : A ⟶ B ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ ran ⁡ F ∈ fi ⁡ B