Theorem onsucunifi

Description: The successor to the union of any non-empty, finite subset of ordinals is the union of the successors of the elements. (Contributed by RP, 12-Feb-2025)

	Ref	Expression
Assertion	onsucunifi	|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> suc U. A = U_ x e. A suc x )

Proof

Step	Hyp	Ref	Expression
1		ordunifi	|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> U. A e. A )
2		suceq	|- ( x = U. A -> suc x = suc U. A )
3	2	ssiun2s	|- ( U. A e. A -> suc U. A C_ U_ x e. A suc x )
4	1 3	syl	|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> suc U. A C_ U_ x e. A suc x )
5		ssorduni	|- ( A C_ On -> Ord U. A )
6		ordsuci	|- ( Ord U. A -> Ord suc U. A )
7	5 6	syl	|- ( A C_ On -> Ord suc U. A )
8		onsucuni	|- ( A C_ On -> A C_ suc U. A )
9	8	sselda	|- ( ( A C_ On /\ x e. A ) -> x e. suc U. A )
10		ordsucss	|- ( Ord suc U. A -> ( x e. suc U. A -> suc x C_ suc U. A ) )
11	10	imp	|- ( ( Ord suc U. A /\ x e. suc U. A ) -> suc x C_ suc U. A )
12	7 9 11	syl2an2r	|- ( ( A C_ On /\ x e. A ) -> suc x C_ suc U. A )
13	12	iunssd	|- ( A C_ On -> U_ x e. A suc x C_ suc U. A )
14	13	3ad2ant1	|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> U_ x e. A suc x C_ suc U. A )
15	4 14	eqssd	|- ( ( A C_ On /\ A e. Fin /\ A =/= (/) ) -> suc U. A = U_ x e. A suc x )