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

Metamath Proof Explorer

Theorem unifi3

Description: If a union is finite, then all its elements are finite. See unifi . (Contributed by Thierry Arnoux, 27-Aug-2017)

		Ref	Expression
	Assertion	unifi3	$⊢ ⋃ A \in Fin \to A \subseteq Fin$

Step	Hyp	Ref	Expression
1		elssuni	$⊢ x \in A \to x \subseteq ⋃ A$
2		ssfi	$⊢ (⋃ A \in Fin \land x \subseteq ⋃ A) \to x \in Fin$
3	2	ex	$⊢ ⋃ A \in Fin \to (x \subseteq ⋃ A \to x \in Fin)$
4	1 3	syl5	$⊢ ⋃ A \in Fin \to (x \in A \to x \in Fin)$
5	4	ssrdv	$⊢ ⋃ A \in Fin \to A \subseteq Fin$