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 \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to ⋂ ran F \in fi (B)$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to F : A ⟶ B$
2	1	frnd	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to ran F \subseteq B$
3	1	fdmd	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to dom F = A$
4		simpr2	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to A \neq \emptyset$
5	3 4	eqnetrd	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to dom F \neq \emptyset$
6		dm0rn0	$⊢ dom F = \emptyset \leftrightarrow ran F = \emptyset$
7	6	necon3bii	$⊢ dom F \neq \emptyset \leftrightarrow ran F \neq \emptyset$
8	5 7	sylib	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to ran F \neq \emptyset$
9		simpr3	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to A \in Fin$
10	1	ffnd	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to F Fn A$
11		dffn4	$⊢ F Fn A \leftrightarrow F : A \underset{onto}{⟶} ran F$
12	10 11	sylib	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to F : A \underset{onto}{⟶} ran F$
13		fofi	$⊢ (A \in Fin \land F : A \underset{onto}{⟶} ran F) \to ran F \in Fin$
14	9 12 13	syl2anc	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to ran F \in Fin$
15	2 8 14	3jca	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to (ran F \subseteq B \land ran F \neq \emptyset \land ran F \in Fin)$
16		elfir	$⊢ (B \in V \land (ran F \subseteq B \land ran F \neq \emptyset \land ran F \in Fin)) \to ⋂ ran F \in fi (B)$
17	15 16	syldan	$⊢ (B \in V \land (F : A ⟶ B \land A \neq \emptyset \land A \in Fin)) \to ⋂ ran F \in fi (B)$