Metamath Proof Explorer

Theorem omcl

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

Ref Expression
Assertion omcl ⊢A∈On∧B∈On→A⋅𝑜B∈On

Proof

Step Hyp Ref Expression
1 oveq2 ⊢x=∅→A⋅𝑜x=A⋅𝑜∅
2 1 eleq1d ⊢x=∅→A⋅𝑜x∈On↔A⋅𝑜∅∈On
3 oveq2 ⊢x=y→A⋅𝑜x=A⋅𝑜y
4 3 eleq1d ⊢x=y→A⋅𝑜x∈On↔A⋅𝑜y∈On
5 oveq2 ⊢x=suc⁡y→A⋅𝑜x=A⋅𝑜suc⁡y
6 5 eleq1d ⊢x=suc⁡y→A⋅𝑜x∈On↔A⋅𝑜suc⁡y∈On
7 oveq2 ⊢x=B→A⋅𝑜x=A⋅𝑜B
8 7 eleq1d ⊢x=B→A⋅𝑜x∈On↔A⋅𝑜B∈On
9 om0 ⊢A∈On→A⋅𝑜∅=∅
10 0elon ⊢∅∈On
11 9 10 eqeltrdi ⊢A∈On→A⋅𝑜∅∈On
12 oacl ⊢A⋅𝑜y∈On∧A∈On→A⋅𝑜y+𝑜A∈On
13 12 expcom ⊢A∈On→A⋅𝑜y∈On→A⋅𝑜y+𝑜A∈On
14 13 adantr ⊢A∈On∧y∈On→A⋅𝑜y∈On→A⋅𝑜y+𝑜A∈On
15 omsuc ⊢A∈On∧y∈On→A⋅𝑜suc⁡y=A⋅𝑜y+𝑜A
16 15 eleq1d ⊢A∈On∧y∈On→A⋅𝑜suc⁡y∈On↔A⋅𝑜y+𝑜A∈On
17 14 16 sylibrd ⊢A∈On∧y∈On→A⋅𝑜y∈On→A⋅𝑜suc⁡y∈On
18 17 expcom ⊢y∈On→A∈On→A⋅𝑜y∈On→A⋅𝑜suc⁡y∈On
19 vex ⊢x∈V
20 iunon ⊢x∈V∧∀y∈xA⋅𝑜y∈On→⋃y∈xA⋅𝑜y∈On
21 19 20 mpan ⊢∀y∈xA⋅𝑜y∈On→⋃y∈xA⋅𝑜y∈On
22 omlim ⊢A∈On∧x∈V∧Lim⁡x→A⋅𝑜x=⋃y∈xA⋅𝑜y
23 19 22 mpanr1 ⊢A∈On∧Lim⁡x→A⋅𝑜x=⋃y∈xA⋅𝑜y
24 23 eleq1d ⊢A∈On∧Lim⁡x→A⋅𝑜x∈On↔⋃y∈xA⋅𝑜y∈On
25 21 24 imbitrrid ⊢A∈On∧Lim⁡x→∀y∈xA⋅𝑜y∈On→A⋅𝑜x∈On
26 25 expcom ⊢Lim⁡x→A∈On→∀y∈xA⋅𝑜y∈On→A⋅𝑜x∈On
27 2 4 6 8 11 18 26 tfinds3 ⊢B∈On→A∈On→A⋅𝑜B∈On
28 27 impcom ⊢A∈On∧B∈On→A⋅𝑜B∈On