Metamath Proof Explorer

Theorem iunon

Description: The indexed union of a set of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003) (Revised by Mario Carneiro, 5-Dec-2016)

		Ref	Expression
	Assertion	iunon	$⊢ (A \in V \land \forall x \in A B \in On) \to ⋃_{x \in A} B \in On$

Proof

Step	Hyp	Ref	Expression
1		dfiun3g	$⊢ \forall x \in A B \in On \to ⋃_{x \in A} B = ⋃ ran (x \in A ⟼ B)$
2	1	adantl	$⊢ (A \in V \land \forall x \in A B \in On) \to ⋃_{x \in A} B = ⋃ ran (x \in A ⟼ B)$
3		mptexg	$⊢ A \in V \to (x \in A ⟼ B) \in V$
4		rnexg	$⊢ (x \in A ⟼ B) \in V \to ran (x \in A ⟼ B) \in V$
5	3 4	syl	$⊢ A \in V \to ran (x \in A ⟼ B) \in V$
6		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
7	6	rnmptss	$⊢ \forall x \in A B \in On \to ran (x \in A ⟼ B) \subseteq On$
8		ssonuni	$⊢ ran (x \in A ⟼ B) \in V \to (ran (x \in A ⟼ B) \subseteq On \to ⋃ ran (x \in A ⟼ B) \in On)$
9	8	imp	$⊢ (ran (x \in A ⟼ B) \in V \land ran (x \in A ⟼ B) \subseteq On) \to ⋃ ran (x \in A ⟼ B) \in On$
10	5 7 9	syl2an	$⊢ (A \in V \land \forall x \in A B \in On) \to ⋃ ran (x \in A ⟼ B) \in On$
11	2 10	eqeltrd	$⊢ (A \in V \land \forall x \in A B \in On) \to ⋃_{x \in A} B \in On$