unfir

Description: If a union is finite, the operands are finite. Converse of unfi . (Contributed by FL, 3-Aug-2009)

		Ref	Expression
	Assertion	unfir	$⊢ A \cup B \in Fin \to (A \in Fin \land B \in Fin)$

Step	Hyp	Ref	Expression
1		ssun1	$⊢ A \subseteq A \cup B$
2		ssfi	$⊢ (A \cup B \in Fin \land A \subseteq A \cup B) \to A \in Fin$
3	1 2	mpan2	$⊢ A \cup B \in Fin \to A \in Fin$
4		ssun2	$⊢ B \subseteq A \cup B$
5		ssfi	$⊢ (A \cup B \in Fin \land B \subseteq A \cup B) \to B \in Fin$
6	4 5	mpan2	$⊢ A \cup B \in Fin \to B \in Fin$
7	3 6	jca	$⊢ A \cup B \in Fin \to (A \in Fin \land B \in Fin)$

Metamath Proof Explorer