Metamath Proof Explorer


Theorem omcl

Description: Closure law for ordinal multiplication. Proposition 8.16 of TakeutiZaring p. 57. (Contributed by NM, 3-Aug-2004) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion omcl ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = ∅ → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o ∅ ) )
2 1 eleq1d ( 𝑥 = ∅ → ( ( 𝐴 ·o 𝑥 ) ∈ On ↔ ( 𝐴 ·o ∅ ) ∈ On ) )
3 oveq2 ( 𝑥 = 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝑦 ) )
4 3 eleq1d ( 𝑥 = 𝑦 → ( ( 𝐴 ·o 𝑥 ) ∈ On ↔ ( 𝐴 ·o 𝑦 ) ∈ On ) )
5 oveq2 ( 𝑥 = suc 𝑦 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o suc 𝑦 ) )
6 5 eleq1d ( 𝑥 = suc 𝑦 → ( ( 𝐴 ·o 𝑥 ) ∈ On ↔ ( 𝐴 ·o suc 𝑦 ) ∈ On ) )
7 oveq2 ( 𝑥 = 𝐵 → ( 𝐴 ·o 𝑥 ) = ( 𝐴 ·o 𝐵 ) )
8 7 eleq1d ( 𝑥 = 𝐵 → ( ( 𝐴 ·o 𝑥 ) ∈ On ↔ ( 𝐴 ·o 𝐵 ) ∈ On ) )
9 om0 ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )
10 0elon ∅ ∈ On
11 9 10 eqeltrdi ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) ∈ On )
12 oacl ( ( ( 𝐴 ·o 𝑦 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ On )
13 12 expcom ( 𝐴 ∈ On → ( ( 𝐴 ·o 𝑦 ) ∈ On → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ On ) )
14 13 adantr ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o 𝑦 ) ∈ On → ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ On ) )
15 omsuc ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( 𝐴 ·o suc 𝑦 ) = ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) )
16 15 eleq1d ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o suc 𝑦 ) ∈ On ↔ ( ( 𝐴 ·o 𝑦 ) +o 𝐴 ) ∈ On ) )
17 14 16 sylibrd ( ( 𝐴 ∈ On ∧ 𝑦 ∈ On ) → ( ( 𝐴 ·o 𝑦 ) ∈ On → ( 𝐴 ·o suc 𝑦 ) ∈ On ) )
18 17 expcom ( 𝑦 ∈ On → ( 𝐴 ∈ On → ( ( 𝐴 ·o 𝑦 ) ∈ On → ( 𝐴 ·o suc 𝑦 ) ∈ On ) ) )
19 vex 𝑥 ∈ V
20 iunon ( ( 𝑥 ∈ V ∧ ∀ 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On ) → 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On )
21 19 20 mpan ( ∀ 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On → 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On )
22 omlim ( ( 𝐴 ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( 𝐴 ·o 𝑥 ) = 𝑦𝑥 ( 𝐴 ·o 𝑦 ) )
23 19 22 mpanr1 ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( 𝐴 ·o 𝑥 ) = 𝑦𝑥 ( 𝐴 ·o 𝑦 ) )
24 23 eleq1d ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( ( 𝐴 ·o 𝑥 ) ∈ On ↔ 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On ) )
25 21 24 syl5ibr ( ( 𝐴 ∈ On ∧ Lim 𝑥 ) → ( ∀ 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On → ( 𝐴 ·o 𝑥 ) ∈ On ) )
26 25 expcom ( Lim 𝑥 → ( 𝐴 ∈ On → ( ∀ 𝑦𝑥 ( 𝐴 ·o 𝑦 ) ∈ On → ( 𝐴 ·o 𝑥 ) ∈ On ) ) )
27 2 4 6 8 11 18 26 tfinds3 ( 𝐵 ∈ On → ( 𝐴 ∈ On → ( 𝐴 ·o 𝐵 ) ∈ On ) )
28 27 impcom ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·o 𝐵 ) ∈ On )