ssorduni

Description: The union of a class of ordinal numbers is ordinal. Proposition 7.19 of TakeutiZaring p. 40. Lemma 2.7 of Schloeder p. 4. (Contributed by NM, 30-May-1994) (Proof shortened by Andrew Salmon, 12-Aug-2011)

		Ref	Expression
	Assertion	ssorduni	$⊢ A \subseteq On \to Ord ⋃ A$

Proof

Step	Hyp	Ref	Expression
1		eluni2	$⊢ x \in ⋃ A \leftrightarrow \exists y \in A x \in y$
2		ssel	$⊢ A \subseteq On \to (y \in A \to y \in On)$
3		onelss	$⊢ y \in On \to (x \in y \to x \subseteq y)$
4	2 3	syl6	$⊢ A \subseteq On \to (y \in A \to (x \in y \to x \subseteq y))$
5		anc2r	$⊢ (y \in A \to (x \in y \to x \subseteq y)) \to (y \in A \to (x \in y \to (x \subseteq y \land y \in A)))$
6	4 5	syl	$⊢ A \subseteq On \to (y \in A \to (x \in y \to (x \subseteq y \land y \in A)))$
7		ssuni	$⊢ (x \subseteq y \land y \in A) \to x \subseteq ⋃ A$
8	6 7	syl8	$⊢ A \subseteq On \to (y \in A \to (x \in y \to x \subseteq ⋃ A))$
9	8	rexlimdv	$⊢ A \subseteq On \to (\exists y \in A x \in y \to x \subseteq ⋃ A)$
10	1 9	biimtrid	$⊢ A \subseteq On \to (x \in ⋃ A \to x \subseteq ⋃ A)$
11	10	ralrimiv	$⊢ A \subseteq On \to \forall x \in ⋃ A x \subseteq ⋃ A$
12		dftr3	$⊢ Tr ⋃ A \leftrightarrow \forall x \in ⋃ A x \subseteq ⋃ A$
13	11 12	sylibr	$⊢ A \subseteq On \to Tr ⋃ A$
14		onelon	$⊢ (y \in On \land x \in y) \to x \in On$
15	14	ex	$⊢ y \in On \to (x \in y \to x \in On)$
16	2 15	syl6	$⊢ A \subseteq On \to (y \in A \to (x \in y \to x \in On))$
17	16	rexlimdv	$⊢ A \subseteq On \to (\exists y \in A x \in y \to x \in On)$
18	1 17	biimtrid	$⊢ A \subseteq On \to (x \in ⋃ A \to x \in On)$
19	18	ssrdv	$⊢ A \subseteq On \to ⋃ A \subseteq On$
20		ordon	$⊢ Ord On$
21		trssord	$⊢ (Tr ⋃ A \land ⋃ A \subseteq On \land Ord On) \to Ord ⋃ A$
22	21	3exp	$⊢ Tr ⋃ A \to (⋃ A \subseteq On \to (Ord On \to Ord ⋃ A))$
23	20 22	mpii	$⊢ Tr ⋃ A \to (⋃ A \subseteq On \to Ord ⋃ A)$
24	13 19 23	sylc	$⊢ A \subseteq On \to Ord ⋃ A$

Metamath Proof Explorer

Theorem ssorduni

Proof