Metamath Proof Explorer

Theorem omordlim

Description: Ordering involving the product of a limit ordinal. Proposition 8.23 of TakeutiZaring p. 64. (Contributed by NM, 25-Dec-2004)

Ref Expression
Assertion omordlim ⊢A∈On∧B∈D∧Lim⁡B∧C∈A⋅𝑜B→∃x∈BC∈A⋅𝑜x

Proof

Step Hyp Ref Expression
1 omlim ⊢A∈On∧B∈D∧Lim⁡B→A⋅𝑜B=⋃x∈BA⋅𝑜x
2 1 eleq2d ⊢A∈On∧B∈D∧Lim⁡B→C∈A⋅𝑜B↔C∈⋃x∈BA⋅𝑜x
3 eliun ⊢C∈⋃x∈BA⋅𝑜x↔∃x∈BC∈A⋅𝑜x
4 2 3 bitrdi ⊢A∈On∧B∈D∧Lim⁡B→C∈A⋅𝑜B↔∃x∈BC∈A⋅𝑜x
5 4 biimpa ⊢A∈On∧B∈D∧Lim⁡B∧C∈A⋅𝑜B→∃x∈BC∈A⋅𝑜x