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	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐷 ∧ Lim 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐴 ·o 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 𝐶 ∈ ( 𝐴 ·o 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		omlim	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐷 ∧ Lim 𝐵 ) ) → ( 𝐴 ·o 𝐵 ) = ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) )
2	1	eleq2d	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐷 ∧ Lim 𝐵 ) ) → ( 𝐶 ∈ ( 𝐴 ·o 𝐵 ) ↔ 𝐶 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) ) )
3		eliun	⊢ ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐵 ( 𝐴 ·o 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐶 ∈ ( 𝐴 ·o 𝑥 ) )
4	2 3	bitrdi	⊢ ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐷 ∧ Lim 𝐵 ) ) → ( 𝐶 ∈ ( 𝐴 ·o 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐵 𝐶 ∈ ( 𝐴 ·o 𝑥 ) ) )
5	4	biimpa	⊢ ( ( ( 𝐴 ∈ On ∧ ( 𝐵 ∈ 𝐷 ∧ Lim 𝐵 ) ) ∧ 𝐶 ∈ ( 𝐴 ·o 𝐵 ) ) → ∃ 𝑥 ∈ 𝐵 𝐶 ∈ ( 𝐴 ·o 𝑥 ) )