Theorem oaabslem

Description: Lemma for oaabs . (Contributed by NM, 9-Dec-2004)

	Ref	Expression
Assertion	oaabslem	|- ( ( _om e. On /\ A e. _om ) -> ( A +o _om ) = _om )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( A e. _om -> A e. On )
2		limom	|- Lim _om
3	2	jctr	|- ( _om e. On -> ( _om e. On /\ Lim _om ) )
4		oalim	|- ( ( A e. On /\ ( _om e. On /\ Lim _om ) ) -> ( A +o _om ) = U_ x e. _om ( A +o x ) )
5	1 3 4	syl2an	|- ( ( A e. _om /\ _om e. On ) -> ( A +o _om ) = U_ x e. _om ( A +o x ) )
6		ordom	|- Ord _om
7		nnacl	|- ( ( A e. _om /\ x e. _om ) -> ( A +o x ) e. _om )
8		ordelss	|- ( ( Ord _om /\ ( A +o x ) e. _om ) -> ( A +o x ) C_ _om )
9	6 7 8	sylancr	|- ( ( A e. _om /\ x e. _om ) -> ( A +o x ) C_ _om )
10	9	ralrimiva	|- ( A e. _om -> A. x e. _om ( A +o x ) C_ _om )
11		iunss	|- ( U_ x e. _om ( A +o x ) C_ _om <-> A. x e. _om ( A +o x ) C_ _om )
12	10 11	sylibr	|- ( A e. _om -> U_ x e. _om ( A +o x ) C_ _om )
13	12	adantr	|- ( ( A e. _om /\ _om e. On ) -> U_ x e. _om ( A +o x ) C_ _om )
14	5 13	eqsstrd	|- ( ( A e. _om /\ _om e. On ) -> ( A +o _om ) C_ _om )
15	14	ancoms	|- ( ( _om e. On /\ A e. _om ) -> ( A +o _om ) C_ _om )
16		oaword2	|- ( ( _om e. On /\ A e. On ) -> _om C_ ( A +o _om ) )
17	1 16	sylan2	|- ( ( _om e. On /\ A e. _om ) -> _om C_ ( A +o _om ) )
18	15 17	eqssd	|- ( ( _om e. On /\ A e. _om ) -> ( A +o _om ) = _om )