unon

Description: The class of all ordinal numbers is its own union. Exercise 11 of TakeutiZaring p. 40. (Contributed by NM, 12-Nov-2003)

		Ref	Expression
	Assertion	unon	$⊢ ⋃ On = On$

Step	Hyp	Ref	Expression
1		eluni2	$⊢ x \in ⋃ On \leftrightarrow \exists y \in On x \in y$
2		onelon	$⊢ (y \in On \land x \in y) \to x \in On$
3	2	rexlimiva	$⊢ \exists y \in On x \in y \to x \in On$
4	1 3	sylbi	$⊢ x \in ⋃ On \to x \in On$
5		vex	$⊢ x \in V$
6	5	sucid	$⊢ x \in suc x$
7		onsuc	$⊢ x \in On \to suc x \in On$
8		elunii	$⊢ (x \in suc x \land suc x \in On) \to x \in ⋃ On$
9	6 7 8	sylancr	$⊢ x \in On \to x \in ⋃ On$
10	4 9	impbii	$⊢ x \in ⋃ On \leftrightarrow x \in On$
11	10	eqriv	$⊢ ⋃ On = On$

Metamath Proof Explorer