Theorem ordunisuc

Description: An ordinal class is equal to the union of its successor. (Contributed by NM, 10-Dec-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	ordunisuc	⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		ordeleqon	⊢ ( Ord 𝐴 ↔ ( 𝐴 ∈ On ∨ 𝐴 = On ) )
2		suceq	⊢ ( 𝑥 = 𝐴 → suc 𝑥 = suc 𝐴 )
3	2	unieqd	⊢ ( 𝑥 = 𝐴 → ∪ suc 𝑥 = ∪ suc 𝐴 )
4		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
5	3 4	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ∪ suc 𝑥 = 𝑥 ↔ ∪ suc 𝐴 = 𝐴 ) )
6		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
7		ordtr	⊢ ( Ord 𝑥 → Tr 𝑥 )
8	6 7	syl	⊢ ( 𝑥 ∈ On → Tr 𝑥 )
9		vex	⊢ 𝑥 ∈ V
10	9	unisuc	⊢ ( Tr 𝑥 ↔ ∪ suc 𝑥 = 𝑥 )
11	8 10	sylib	⊢ ( 𝑥 ∈ On → ∪ suc 𝑥 = 𝑥 )
12	5 11	vtoclga	⊢ ( 𝐴 ∈ On → ∪ suc 𝐴 = 𝐴 )
13		sucon	⊢ suc On = On
14	13	unieqi	⊢ ∪ suc On = ∪ On
15		unon	⊢ ∪ On = On
16	14 15	eqtri	⊢ ∪ suc On = On
17		suceq	⊢ ( 𝐴 = On → suc 𝐴 = suc On )
18	17	unieqd	⊢ ( 𝐴 = On → ∪ suc 𝐴 = ∪ suc On )
19		id	⊢ ( 𝐴 = On → 𝐴 = On )
20	16 18 19	3eqtr4a	⊢ ( 𝐴 = On → ∪ suc 𝐴 = 𝐴 )
21	12 20	jaoi	⊢ ( ( 𝐴 ∈ On ∨ 𝐴 = On ) → ∪ suc 𝐴 = 𝐴 )
22	1 21	sylbi	⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )