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 ‘ 𝐵 ) )