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	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ suc ( 𝐴 +o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		oaun3lem2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) )
2		oaun3lem3	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ On )
3		oacl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
4		onsssuc	⊢ ( ( { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ On ∧ ( 𝐴 +o 𝐵 ) ∈ On ) → ( { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) ↔ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ suc ( 𝐴 +o 𝐵 ) ) )
5	2 3 4	syl2anc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) ↔ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ suc ( 𝐴 +o 𝐵 ) ) )
6	1 5	mpbid	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ suc ( 𝐴 +o 𝐵 ) )