Metamath Proof Explorer

Theorem unirnffid

Description: The union of the range of a function from a finite set into the class of finite sets is finite. Deduction form. (Contributed by David Moews, 1-May-2017)

		Ref	Expression
	Hypotheses	unirnffid.1	$⊢ φ \to F : T ⟶ Fin$
		unirnffid.2	$⊢ φ \to T \in Fin$
	Assertion	unirnffid	$⊢ φ \to ⋃ ran F \in Fin$

Proof

Step	Hyp	Ref	Expression
1		unirnffid.1	$⊢ φ \to F : T ⟶ Fin$
2		unirnffid.2	$⊢ φ \to T \in Fin$
3	1	ffnd	$⊢ φ \to F Fn T$
4		fnfi	$⊢ (F Fn T \land T \in Fin) \to F \in Fin$
5	3 2 4	syl2anc	$⊢ φ \to F \in Fin$
6		rnfi	$⊢ F \in Fin \to ran F \in Fin$
7	5 6	syl	$⊢ φ \to ran F \in Fin$
8	1	frnd	$⊢ φ \to ran F \subseteq Fin$
9		unifi	$⊢ (ran F \in Fin \land ran F \subseteq Fin) \to ⋃ ran F \in Fin$
10	7 8 9	syl2anc	$⊢ φ \to ⋃ ran F \in Fin$