Theorem omord2lim

Description: Given a limit ordinal, the product of any non-zero ordinal with an ordinal less than that limit ordinal is less than the product of the non-zero ordinal with the limit ordinal . Lemma 3.14 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		limord	⊢ ( Lim 𝐶 → Ord 𝐶 )
2	1	ad2antrl	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → Ord 𝐶 )
3		ordelon	⊢ ( ( Ord 𝐶 ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ On )
4	2 3	sylan	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ On )
5		elex	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 ∈ V )
6	1 5	anim12i	⊢ ( ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) → ( Ord 𝐶 ∧ 𝐶 ∈ V ) )
7	6	ad2antlr	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → ( Ord 𝐶 ∧ 𝐶 ∈ V ) )
8		elon2	⊢ ( 𝐶 ∈ On ↔ ( Ord 𝐶 ∧ 𝐶 ∈ V ) )
9	7 8	sylibr	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → 𝐶 ∈ On )
10		simplll	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → 𝐴 ∈ On )
11		simpr	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → 𝐵 ∈ 𝐶 )
12		on0eln0	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ↔ 𝐴 ≠ ∅ ) )
13	12	biimpar	⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) → ∅ ∈ 𝐴 )
14	13	ad2antrr	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → ∅ ∈ 𝐴 )
15		omord	⊢ ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ↔ ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )
16	15	biimpa	⊢ ( ( ( 𝐵 ∈ On ∧ 𝐶 ∈ On ∧ 𝐴 ∈ On ) ∧ ( 𝐵 ∈ 𝐶 ∧ ∅ ∈ 𝐴 ) ) → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) )
17	4 9 10 11 14 16	syl32anc	⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) )
18	17	ex	⊢ ( ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ) ∧ ( Lim 𝐶 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 ∈ 𝐶 → ( 𝐴 ·o 𝐵 ) ∈ ( 𝐴 ·o 𝐶 ) ) )