Theorem oaun2

Description: Ordinal addition as a union of classes. (Contributed by RP, 13-Feb-2025)

	Ref	Expression
Assertion	oaun2	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } } )

Proof

Step	Hyp	Ref	Expression
1		oacl	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
2	1	difexd	|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) \ A ) e. _V )
3		uniprg	|- ( ( A e. On /\ ( ( A +o B ) \ A ) e. _V ) -> U. { A , ( ( A +o B ) \ A ) } = ( A u. ( ( A +o B ) \ A ) ) )
4	2 3	syldan	|- ( ( A e. On /\ B e. On ) -> U. { A , ( ( A +o B ) \ A ) } = ( A u. ( ( A +o B ) \ A ) ) )
5		rp-abid	|- A = { x | E. a e. A x = a }
6	5	a1i	|- ( ( A e. On /\ B e. On ) -> A = { x | E. a e. A x = a } )
7		oadif1	|- ( ( A e. On /\ B e. On ) -> ( ( A +o B ) \ A ) = { y | E. b e. B y = ( A +o b ) } )
8	6 7	preq12d	|- ( ( A e. On /\ B e. On ) -> { A , ( ( A +o B ) \ A ) } = { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } } )
9	8	unieqd	|- ( ( A e. On /\ B e. On ) -> U. { A , ( ( A +o B ) \ A ) } = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } } )
10		undif2	|- ( A u. ( ( A +o B ) \ A ) ) = ( A u. ( A +o B ) )
11		oaword1	|- ( ( A e. On /\ B e. On ) -> A C_ ( A +o B ) )
12		ssequn1	|- ( A C_ ( A +o B ) <-> ( A u. ( A +o B ) ) = ( A +o B ) )
13	11 12	sylib	|- ( ( A e. On /\ B e. On ) -> ( A u. ( A +o B ) ) = ( A +o B ) )
14	10 13	eqtrid	|- ( ( A e. On /\ B e. On ) -> ( A u. ( ( A +o B ) \ A ) ) = ( A +o B ) )
15	4 9 14	3eqtr3rd	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = U. { { x | E. a e. A x = a } , { y | E. b e. B y = ( A +o b ) } } )