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 )