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	|- ( ph -> F : T --> Fin )
	unirnffid.2	|- ( ph -> T e. Fin )
Assertion	unirnffid	|- ( ph -> U. ran F e. Fin )

Proof

Step	Hyp	Ref	Expression
1		unirnffid.1	|- ( ph -> F : T --> Fin )
2		unirnffid.2	|- ( ph -> T e. Fin )
3	1	ffnd	|- ( ph -> F Fn T )
4		fnfi	|- ( ( F Fn T /\ T e. Fin ) -> F e. Fin )
5	3 2 4	syl2anc	|- ( ph -> F e. Fin )
6		rnfi	|- ( F e. Fin -> ran F e. Fin )
7	5 6	syl	|- ( ph -> ran F e. Fin )
8	1	frnd	|- ( ph -> ran F C_ Fin )
9		unifi	|- ( ( ran F e. Fin /\ ran F C_ Fin ) -> U. ran F e. Fin )
10	7 8 9	syl2anc	|- ( ph -> U. ran F e. Fin )