Theorem onsucunipr

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

	Ref	Expression
Assertion	onsucunipr	|- ( ( A e. On /\ B e. On ) -> suc U. { A , B } = U. { suc A , suc B } )

Proof

Step	Hyp	Ref	Expression
1		ssequn1	|- ( A C_ B <-> ( A u. B ) = B )
2		suceq	|- ( ( A u. B ) = B -> suc ( A u. B ) = suc B )
3	1 2	sylbi	|- ( A C_ B -> suc ( A u. B ) = suc B )
4	3	adantl	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> suc ( A u. B ) = suc B )
5		onsucwordi	|- ( ( A e. On /\ B e. On ) -> ( A C_ B -> suc A C_ suc B ) )
6	5	imp	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> suc A C_ suc B )
7		ssequn1	|- ( suc A C_ suc B <-> ( suc A u. suc B ) = suc B )
8	6 7	sylib	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> ( suc A u. suc B ) = suc B )
9	4 8	eqtr4d	|- ( ( ( A e. On /\ B e. On ) /\ A C_ B ) -> suc ( A u. B ) = ( suc A u. suc B ) )
10		ssequn2	|- ( B C_ A <-> ( A u. B ) = A )
11		suceq	|- ( ( A u. B ) = A -> suc ( A u. B ) = suc A )
12	10 11	sylbi	|- ( B C_ A -> suc ( A u. B ) = suc A )
13	12	adantl	|- ( ( ( A e. On /\ B e. On ) /\ B C_ A ) -> suc ( A u. B ) = suc A )
14		onsucwordi	|- ( ( B e. On /\ A e. On ) -> ( B C_ A -> suc B C_ suc A ) )
15	14	ancoms	|- ( ( A e. On /\ B e. On ) -> ( B C_ A -> suc B C_ suc A ) )
16	15	imp	|- ( ( ( A e. On /\ B e. On ) /\ B C_ A ) -> suc B C_ suc A )
17		ssequn2	|- ( suc B C_ suc A <-> ( suc A u. suc B ) = suc A )
18	16 17	sylib	|- ( ( ( A e. On /\ B e. On ) /\ B C_ A ) -> ( suc A u. suc B ) = suc A )
19	13 18	eqtr4d	|- ( ( ( A e. On /\ B e. On ) /\ B C_ A ) -> suc ( A u. B ) = ( suc A u. suc B ) )
20		eloni	|- ( A e. On -> Ord A )
21		eloni	|- ( B e. On -> Ord B )
22		ordtri2or2	|- ( ( Ord A /\ Ord B ) -> ( A C_ B \/ B C_ A ) )
23	20 21 22	syl2an	|- ( ( A e. On /\ B e. On ) -> ( A C_ B \/ B C_ A ) )
24	9 19 23	mpjaodan	|- ( ( A e. On /\ B e. On ) -> suc ( A u. B ) = ( suc A u. suc B ) )
25		uniprg	|- ( ( A e. On /\ B e. On ) -> U. { A , B } = ( A u. B ) )
26		suceq	|- ( U. { A , B } = ( A u. B ) -> suc U. { A , B } = suc ( A u. B ) )
27	25 26	syl	|- ( ( A e. On /\ B e. On ) -> suc U. { A , B } = suc ( A u. B ) )
28		onsuc	|- ( A e. On -> suc A e. On )
29		onsuc	|- ( B e. On -> suc B e. On )
30		uniprg	|- ( ( suc A e. On /\ suc B e. On ) -> U. { suc A , suc B } = ( suc A u. suc B ) )
31	28 29 30	syl2an	|- ( ( A e. On /\ B e. On ) -> U. { suc A , suc B } = ( suc A u. suc B ) )
32	24 27 31	3eqtr4d	|- ( ( A e. On /\ B e. On ) -> suc U. { A , B } = U. { suc A , suc B } )