Theorem 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

Proof

Step	Hyp	Ref	Expression
1		eluni2	⊢ ( 𝑥 ∈ ∪ On ↔ ∃ 𝑦 ∈ On 𝑥 ∈ 𝑦 )
2		onelon	⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ 𝑦 ) → 𝑥 ∈ On )
3	2	rexlimiva	⊢ ( ∃ 𝑦 ∈ On 𝑥 ∈ 𝑦 → 𝑥 ∈ On )
4	1 3	sylbi	⊢ ( 𝑥 ∈ ∪ On → 𝑥 ∈ On )
5		vex	⊢ 𝑥 ∈ V
6	5	sucid	⊢ 𝑥 ∈ suc 𝑥
7		suceloni	⊢ ( 𝑥 ∈ On → suc 𝑥 ∈ On )
8		elunii	⊢ ( ( 𝑥 ∈ suc 𝑥 ∧ suc 𝑥 ∈ On ) → 𝑥 ∈ ∪ On )
9	6 7 8	sylancr	⊢ ( 𝑥 ∈ On → 𝑥 ∈ ∪ On )
10	4 9	impbii	⊢ ( 𝑥 ∈ ∪ On ↔ 𝑥 ∈ On )
11	10	eqriv	⊢ ∪ On = On