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

Proof

Step	Hyp	Ref	Expression
1		oaun3lem1	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → Ord { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } )
2		oacl	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) ∈ On )
3		oaun3lem2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ⊆ ( 𝐴 +o 𝐵 ) )
4	2 3	ssexd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ V )
5		elon2	⊢ ( { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ On ↔ ( Ord { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∧ { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ V ) )
6	1 4 5	sylanbrc	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → { 𝑥 ∣ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 𝑥 = ( 𝑎 +o 𝑏 ) } ∈ On )