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 e. On /\ ( B e. D /\ Lim B ) ) /\ C e. ( A .o B ) ) -> E. x e. B C e. ( A .o x ) )

Proof

Step Hyp Ref Expression
1 omlim 
 |-  ( ( A e. On /\ ( B e. D /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )
2 1 eleq2d 
 |-  ( ( A e. On /\ ( B e. D /\ Lim B ) ) -> ( C e. ( A .o B ) <-> C e. U_ x e. B ( A .o x ) ) )
3 eliun 
 |-  ( C e. U_ x e. B ( A .o x ) <-> E. x e. B C e. ( A .o x ) )
4 2 3 bitrdi 
 |-  ( ( A e. On /\ ( B e. D /\ Lim B ) ) -> ( C e. ( A .o B ) <-> E. x e. B C e. ( A .o x ) ) )
5 4 biimpa 
 |-  ( ( ( A e. On /\ ( B e. D /\ Lim B ) ) /\ C e. ( A .o B ) ) -> E. x e. B C e. ( A .o x ) )