This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ ran 𝐹 ∈ ( fi ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
2 1 frnd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ran 𝐹 ⊆ 𝐵 )
3 1 fdmd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → dom 𝐹 = 𝐴 )
4 simpr2 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐴 ≠ ∅ )
5 3 4 eqnetrd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → dom 𝐹 ≠ ∅ )
6 dm0rn0 ⊢ ( dom 𝐹 = ∅ ↔ ran 𝐹 = ∅ )
7 6 necon3bii ⊢ ( dom 𝐹 ≠ ∅ ↔ ran 𝐹 ≠ ∅ )
8 5 7 sylib ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ran 𝐹 ≠ ∅ )
9 simpr3 ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐴 ∈ Fin )
10 1 ffnd ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐹 Fn 𝐴 )
11 dffn4 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 –onto→ ran 𝐹 )
12 10 11 sylib ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → 𝐹 : 𝐴 –onto→ ran 𝐹 )
13 fofi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐹 : 𝐴 –onto→ ran 𝐹 ) → ran 𝐹 ∈ Fin )
14 9 12 13 syl2anc ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ran 𝐹 ∈ Fin )
15 2 8 14 3jca ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ≠ ∅ ∧ ran 𝐹 ∈ Fin ) )
16 elfir ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ≠ ∅ ∧ ran 𝐹 ∈ Fin ) ) → ∩ ran 𝐹 ∈ ( fi ‘ 𝐵 ) )
17 15 16 syldan ⊢ ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ ran 𝐹 ∈ ( fi ‘ 𝐵 ) )