Theorem oaun3lem3

Description: The class of all ordinal sums of elements from two ordinals is an ordinal. Lemma for oaun3 . (Contributed by RP, 13-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oaun3lem1	|- ( ( A e. On /\ B e. On ) -> Ord { x | E. a e. A E. b e. B x = ( a +o b ) } )
2		oacl	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
3		oaun3lem2	|- ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } C_ ( A +o B ) )
4	2 3	ssexd	|- ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } e. _V )
5		elon2	|- ( { x | E. a e. A E. b e. B x = ( a +o b ) } e. On <-> ( Ord { x | E. a e. A E. b e. B x = ( a +o b ) } /\ { x | E. a e. A E. b e. B x = ( a +o b ) } e. _V ) )
6	1 4 5	sylanbrc	|- ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } e. On )