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	|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim B /\ B e. V ) ) -> Lim ( A .o B ) )

Proof

Step	Hyp	Ref	Expression
1		simpll	|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim B /\ B e. V ) ) -> A e. On )
2		simpr	|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim B /\ B e. V ) ) -> ( Lim B /\ B e. V ) )
3	2	ancomd	|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim B /\ B e. V ) ) -> ( B e. V /\ Lim B ) )
4		on0eln0	|- ( A e. On -> ( (/) e. A <-> A =/= (/) ) )
5	4	biimpar	|- ( ( A e. On /\ A =/= (/) ) -> (/) e. A )
6	5	adantr	|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim B /\ B e. V ) ) -> (/) e. A )
7		omlimcl	|- ( ( ( A e. On /\ ( B e. V /\ Lim B ) ) /\ (/) e. A ) -> Lim ( A .o B ) )
8	1 3 6 7	syl21anc	|- ( ( ( A e. On /\ A =/= (/) ) /\ ( Lim B /\ B e. V ) ) -> Lim ( A .o B ) )