This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem omlim

Description: Ordinal multiplication with a limit ordinal. Definition 8.15 of TakeutiZaring p. 62. Definition 2.5 of Schloeder p. 4. (Contributed by NM, 3-Aug-2004) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion omlim 
|- ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )

Proof

Step Hyp Ref Expression
1 limelon 
 |-  ( ( B e. C /\ Lim B ) -> B e. On )
2 simpr 
 |-  ( ( B e. C /\ Lim B ) -> Lim B )
3 1 2 jca 
 |-  ( ( B e. C /\ Lim B ) -> ( B e. On /\ Lim B ) )
4 rdglim2a 
 |-  ( ( B e. On /\ Lim B ) -> ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) )
5 4 adantl 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) )
6 omv 
 |-  ( ( A e. On /\ B e. On ) -> ( A .o B ) = ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` B ) )
7 onelon 
 |-  ( ( B e. On /\ x e. B ) -> x e. On )
8 omv 
 |-  ( ( A e. On /\ x e. On ) -> ( A .o x ) = ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) )
9 7 8 sylan2 
 |-  ( ( A e. On /\ ( B e. On /\ x e. B ) ) -> ( A .o x ) = ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) )
10 9 anassrs 
 |-  ( ( ( A e. On /\ B e. On ) /\ x e. B ) -> ( A .o x ) = ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) )
11 10 iuneq2dv 
 |-  ( ( A e. On /\ B e. On ) -> U_ x e. B ( A .o x ) = U_ x e. B ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) )
12 6 11 eqeq12d 
 |-  ( ( A e. On /\ B e. On ) -> ( ( A .o B ) = U_ x e. B ( A .o x ) <-> ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) ) )
13 12 adantrr 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( ( A .o B ) = U_ x e. B ( A .o x ) <-> ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> ( y +o A ) ) , (/) ) ` x ) ) )
14 5 13 mpbird 
 |-  ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )
15 3 14 sylan2 
 |-  ( ( A e. On /\ ( B e. C /\ Lim B ) ) -> ( A .o B ) = U_ x e. B ( A .o x ) )