Theorem omlim2

Description: The non-zero product with an limit ordinal on the right is a limit ordinal. Lemma 3.13 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

	Ref	Expression
Assertion	omlim2	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → Lim ( 𝐴 ·o 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ On )
2		simpr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) )
3	2	ancomd	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐵 ∈ 𝑉 ∧ Lim 𝐵 ) )
4		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
5	4	biimpar	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) → ∅ ∈ 𝐴 )
6	5	adantr	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → ∅ ∈ 𝐴 )
7		omlimcl	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝑉 ∧ Lim 𝐵 ) ) ∧ ∅ ∈ 𝐴 ) → Lim ( 𝐴 ·o 𝐵 ) )
8	1 3 6 7	syl21anc	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐵 ∧ 𝐵 ∈ 𝑉 ) ) → Lim ( 𝐴 ·o 𝐵 ) )