Theorem onsucunitp

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

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

Proof

Step	Hyp	Ref	Expression
1		onun2	|- ( ( A e. On /\ B e. On ) -> ( A u. B ) e. On )
2		onsucunipr	|- ( ( ( A u. B ) e. On /\ C e. On ) -> suc U. { ( A u. B ) , C } = U. { suc ( A u. B ) , suc C } )
3	1 2	sylan	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> suc U. { ( A u. B ) , C } = U. { suc ( A u. B ) , suc C } )
4		uniprg	|- ( ( A e. On /\ B e. On ) -> U. { A , B } = ( A u. B ) )
5	4	adantr	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { A , B } = ( A u. B ) )
6		unisng	|- ( C e. On -> U. { C } = C )
7	6	adantl	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { C } = C )
8	5 7	uneq12d	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( U. { A , B } u. U. { C } ) = ( ( A u. B ) u. C ) )
9		df-tp	|- { A , B , C } = ( { A , B } u. { C } )
10	9	unieqi	|- U. { A , B , C } = U. ( { A , B } u. { C } )
11		uniun	|- U. ( { A , B } u. { C } ) = ( U. { A , B } u. U. { C } )
12	10 11	eqtri	|- U. { A , B , C } = ( U. { A , B } u. U. { C } )
13	12	a1i	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { A , B , C } = ( U. { A , B } u. U. { C } ) )
14		uniprg	|- ( ( ( A u. B ) e. On /\ C e. On ) -> U. { ( A u. B ) , C } = ( ( A u. B ) u. C ) )
15	1 14	sylan	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { ( A u. B ) , C } = ( ( A u. B ) u. C ) )
16	8 13 15	3eqtr4d	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { A , B , C } = U. { ( A u. B ) , C } )
17		suceq	|- ( U. { A , B , C } = U. { ( A u. B ) , C } -> suc U. { A , B , C } = suc U. { ( A u. B ) , C } )
18	16 17	syl	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> suc U. { A , B , C } = suc U. { ( A u. B ) , C } )
19		df-tp	|- { suc A , suc B , suc C } = ( { suc A , suc B } u. { suc C } )
20	19	unieqi	|- U. { suc A , suc B , suc C } = U. ( { suc A , suc B } u. { suc C } )
21		uniun	|- U. ( { suc A , suc B } u. { suc C } ) = ( U. { suc A , suc B } u. U. { suc C } )
22	20 21	eqtri	|- U. { suc A , suc B , suc C } = ( U. { suc A , suc B } u. U. { suc C } )
23		onsuc	|- ( ( A u. B ) e. On -> suc ( A u. B ) e. On )
24	1 23	syl	|- ( ( A e. On /\ B e. On ) -> suc ( A u. B ) e. On )
25		onsuc	|- ( C e. On -> suc C e. On )
26		uniprg	|- ( ( suc ( A u. B ) e. On /\ suc C e. On ) -> U. { suc ( A u. B ) , suc C } = ( suc ( A u. B ) u. suc C ) )
27	24 25 26	syl2an	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { suc ( A u. B ) , suc C } = ( suc ( A u. B ) u. suc C ) )
28		suceq	|- ( U. { A , B } = ( A u. B ) -> suc U. { A , B } = suc ( A u. B ) )
29	4 28	syl	|- ( ( A e. On /\ B e. On ) -> suc U. { A , B } = suc ( A u. B ) )
30		onsucunipr	|- ( ( A e. On /\ B e. On ) -> suc U. { A , B } = U. { suc A , suc B } )
31	29 30	eqtr3d	|- ( ( A e. On /\ B e. On ) -> suc ( A u. B ) = U. { suc A , suc B } )
32	31	adantr	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> suc ( A u. B ) = U. { suc A , suc B } )
33		unisng	|- ( suc C e. On -> U. { suc C } = suc C )
34	25 33	syl	|- ( C e. On -> U. { suc C } = suc C )
35	34	eqcomd	|- ( C e. On -> suc C = U. { suc C } )
36	35	adantl	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> suc C = U. { suc C } )
37	32 36	uneq12d	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> ( suc ( A u. B ) u. suc C ) = ( U. { suc A , suc B } u. U. { suc C } ) )
38	27 37	eqtrd	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { suc ( A u. B ) , suc C } = ( U. { suc A , suc B } u. U. { suc C } ) )
39	22 38	eqtr4id	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> U. { suc A , suc B , suc C } = U. { suc ( A u. B ) , suc C } )
40	3 18 39	3eqtr4d	|- ( ( ( A e. On /\ B e. On ) /\ C e. On ) -> suc U. { A , B , C } = U. { suc A , suc B , suc C } )
41	40	3impa	|- ( ( A e. On /\ B e. On /\ C e. On ) -> suc U. { A , B , C } = U. { suc A , suc B , suc C } )