Theorem onsucuni2

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

	Ref	Expression
Assertion	onsucuni2	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝐴 = suc 𝐵 → ( 𝐴 ∈ On ↔ suc 𝐵 ∈ On ) )
2	1	biimpac	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc 𝐵 ∈ On )
3		eloni	⊢ ( suc 𝐵 ∈ On → Ord suc 𝐵 )
4		ordsuc	⊢ ( Ord 𝐵 ↔ Ord suc 𝐵 )
5		ordunisuc	⊢ ( Ord 𝐵 → ∪ suc 𝐵 = 𝐵 )
6	4 5	sylbir	⊢ ( Ord suc 𝐵 → ∪ suc 𝐵 = 𝐵 )
7		suceq	⊢ ( ∪ suc 𝐵 = 𝐵 → suc ∪ suc 𝐵 = suc 𝐵 )
8	6 7	syl	⊢ ( Ord suc 𝐵 → suc ∪ suc 𝐵 = suc 𝐵 )
9		ordunisuc	⊢ ( Ord suc 𝐵 → ∪ suc suc 𝐵 = suc 𝐵 )
10	8 9	eqtr4d	⊢ ( Ord suc 𝐵 → suc ∪ suc 𝐵 = ∪ suc suc 𝐵 )
11	2 3 10	3syl	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ suc 𝐵 = ∪ suc suc 𝐵 )
12		unieq	⊢ ( 𝐴 = suc 𝐵 → ∪ 𝐴 = ∪ suc 𝐵 )
13		suceq	⊢ ( ∪ 𝐴 = ∪ suc 𝐵 → suc ∪ 𝐴 = suc ∪ suc 𝐵 )
14	12 13	syl	⊢ ( 𝐴 = suc 𝐵 → suc ∪ 𝐴 = suc ∪ suc 𝐵 )
15		suceq	⊢ ( 𝐴 = suc 𝐵 → suc 𝐴 = suc suc 𝐵 )
16	15	unieqd	⊢ ( 𝐴 = suc 𝐵 → ∪ suc 𝐴 = ∪ suc suc 𝐵 )
17	14 16	eqeq12d	⊢ ( 𝐴 = suc 𝐵 → ( suc ∪ 𝐴 = ∪ suc 𝐴 ↔ suc ∪ suc 𝐵 = ∪ suc suc 𝐵 ) )
18	11 17	imbitrrid	⊢ ( 𝐴 = suc 𝐵 → ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = ∪ suc 𝐴 ) )
19	18	anabsi7	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = ∪ suc 𝐴 )
20		eloni	⊢ ( 𝐴 ∈ On → Ord 𝐴 )
21		ordunisuc	⊢ ( Ord 𝐴 → ∪ suc 𝐴 = 𝐴 )
22	20 21	syl	⊢ ( 𝐴 ∈ On → ∪ suc 𝐴 = 𝐴 )
23	22	adantr	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → ∪ suc 𝐴 = 𝐴 )
24	19 23	eqtrd	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 = suc 𝐵 ) → suc ∪ 𝐴 = 𝐴 )