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 ∈ B C ∈ A ⋅ 𝑜 x

Proof

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