iunord

Description: The indexed union of a collection of ordinal numbers B ( x ) is ordinal. This proof is based on the proof of ssorduni , but does not use it directly, since ssorduni does not work when B is a proper class. (Contributed by Emmett Weisz, 3-Nov-2019)

		Ref	Expression
	Assertion	iunord	$⊢ \forall x \in A Ord B \to Ord ⋃_{x \in A} B$

Proof

Step	Hyp	Ref	Expression
1		ordtr	$⊢ Ord B \to Tr B$
2	1	ralimi	$⊢ \forall x \in A Ord B \to \forall x \in A Tr B$
3		triun	$⊢ \forall x \in A Tr B \to Tr ⋃_{x \in A} B$
4	2 3	syl	$⊢ \forall x \in A Ord B \to Tr ⋃_{x \in A} B$
5		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
6		nfra1	$⊢ Ⅎ x \forall x \in A Ord B$
7		nfv	$⊢ Ⅎ x y \in On$
8		rsp	$⊢ \forall x \in A Ord B \to (x \in A \to Ord B)$
9		ordelon	$⊢ (Ord B \land y \in B) \to y \in On$
10	9	ex	$⊢ Ord B \to (y \in B \to y \in On)$
11	8 10	syl6	$⊢ \forall x \in A Ord B \to (x \in A \to (y \in B \to y \in On))$
12	6 7 11	rexlimd	$⊢ \forall x \in A Ord B \to (\exists x \in A y \in B \to y \in On)$
13	5 12	biimtrid	$⊢ \forall x \in A Ord B \to (y \in ⋃_{x \in A} B \to y \in On)$
14	13	ssrdv	$⊢ \forall x \in A Ord B \to ⋃_{x \in A} B \subseteq On$
15		ordon	$⊢ Ord On$
16		trssord	$⊢ (Tr ⋃_{x \in A} B \land ⋃_{x \in A} B \subseteq On \land Ord On) \to Ord ⋃_{x \in A} B$
17	16	3exp	$⊢ Tr ⋃_{x \in A} B \to (⋃_{x \in A} B \subseteq On \to (Ord On \to Ord ⋃_{x \in A} B))$
18	15 17	mpii	$⊢ Tr ⋃_{x \in A} B \to (⋃_{x \in A} B \subseteq On \to Ord ⋃_{x \in A} B)$
19	4 14 18	sylc	$⊢ \forall x \in A Ord B \to Ord ⋃_{x \in A} B$

Metamath Proof Explorer

Theorem iunord

Proof