Metamath Proof Explorer

Theorem unifi2

Description: The finite union of finite sets is finite. Exercise 13 of Enderton p. 144. This version of unifi is useful only if we assume the Axiom of Infinity (see comments in fin2inf ). (Contributed by NM, 11-Mar-2006)

		Ref	Expression
	Assertion	unifi2	$⊢ (A ≺ ω \land \forall x \in A x ≺ ω) \to ⋃ A ≺ ω$

Proof

Step	Hyp	Ref	Expression
1		isfinite2	$⊢ A ≺ ω \to A \in Fin$
2		isfinite2	$⊢ x ≺ ω \to x \in Fin$
3	2	ralimi	$⊢ \forall x \in A x ≺ ω \to \forall x \in A x \in Fin$
4		dfss3	$⊢ A \subseteq Fin \leftrightarrow \forall x \in A x \in Fin$
5	3 4	sylibr	$⊢ \forall x \in A x ≺ ω \to A \subseteq Fin$
6		unifi	$⊢ (A \in Fin \land A \subseteq Fin) \to ⋃ A \in Fin$
7	1 5 6	syl2an	$⊢ (A ≺ ω \land \forall x \in A x ≺ ω) \to ⋃ A \in Fin$
8		fin2inf	$⊢ A ≺ ω \to ω \in V$
9	8	adantr	$⊢ (A ≺ ω \land \forall x \in A x ≺ ω) \to ω \in V$
10		isfiniteg	$⊢ ω \in V \to (⋃ A \in Fin \leftrightarrow ⋃ A ≺ ω)$
11	9 10	syl	$⊢ (A ≺ ω \land \forall x \in A x ≺ ω) \to (⋃ A \in Fin \leftrightarrow ⋃ A ≺ ω)$
12	7 11	mpbid	$⊢ (A ≺ ω \land \forall x \in A x ≺ ω) \to ⋃ A ≺ ω$