Theorem oaun3lem4

Description: The class of all ordinal sums of elements from two ordinals is less than the successor to the sum. Lemma for oaun3 . (Contributed by RP, 12-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oaun3lem2	|- ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } C_ ( A +o B ) )
2		oaun3lem3	|- ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } e. On )
3		oacl	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) e. On )
4		onsssuc	|- ( ( { x | E. a e. A E. b e. B x = ( a +o b ) } e. On /\ ( A +o B ) e. On ) -> ( { x | E. a e. A E. b e. B x = ( a +o b ) } C_ ( A +o B ) <-> { x | E. a e. A E. b e. B x = ( a +o b ) } e. suc ( A +o B ) ) )
5	2 3 4	syl2anc	|- ( ( A e. On /\ B e. On ) -> ( { x | E. a e. A E. b e. B x = ( a +o b ) } C_ ( A +o B ) <-> { x | E. a e. A E. b e. B x = ( a +o b ) } e. suc ( A +o B ) ) )
6	1 5	mpbid	|- ( ( A e. On /\ B e. On ) -> { x | E. a e. A E. b e. B x = ( a +o b ) } e. suc ( A +o B ) )