Theorem oalim

Description: Ordinal addition with a limit ordinal. Definition 8.1 of TakeutiZaring p. 56. (Contributed by NM, 3-Aug-2004) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	oalim	|- ( ( 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 |-> suc y ) , A ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> suc y ) , A ) ` x ) )
5	4	adantl	|- ( ( A e. On /\ ( B e. On /\ Lim B ) ) -> ( rec ( ( y e. _V |-> suc y ) , A ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> suc y ) , A ) ` x ) )
6		oav	|- ( ( A e. On /\ B e. On ) -> ( A +o B ) = ( rec ( ( y e. _V |-> suc y ) , A ) ` B ) )
7		onelon	|- ( ( B e. On /\ x e. B ) -> x e. On )
8		oav	|- ( ( A e. On /\ x e. On ) -> ( A +o x ) = ( rec ( ( y e. _V |-> suc y ) , A ) ` x ) )
9	7 8	sylan2	|- ( ( A e. On /\ ( B e. On /\ x e. B ) ) -> ( A +o x ) = ( rec ( ( y e. _V |-> suc y ) , A ) ` x ) )
10	9	anassrs	|- ( ( ( A e. On /\ B e. On ) /\ x e. B ) -> ( A +o x ) = ( rec ( ( y e. _V |-> suc y ) , 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 |-> suc y ) , 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 |-> suc y ) , A ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> suc y ) , 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 |-> suc y ) , A ) ` B ) = U_ x e. B ( rec ( ( y e. _V |-> suc y ) , 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 ) )