Theorem omabslem

Description: Lemma for omabs . (Contributed by Mario Carneiro, 30-May-2015)

	Ref	Expression
Assertion	omabslem	|- ( ( _om e. On /\ A e. _om /\ (/) e. A ) -> ( 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		omlim	|- ( ( 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		nnmcl	|- ( ( 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	15	3adant3	|- ( ( _om e. On /\ A e. _om /\ (/) e. A ) -> ( A .o _om ) C_ _om )
17		omword2	|- ( ( ( _om e. On /\ A e. On ) /\ (/) e. A ) -> _om C_ ( A .o _om ) )
18	17	3impa	|- ( ( _om e. On /\ A e. On /\ (/) e. A ) -> _om C_ ( A .o _om ) )
19	1 18	syl3an2	|- ( ( _om e. On /\ A e. _om /\ (/) e. A ) -> _om C_ ( A .o _om ) )
20	16 19	eqssd	|- ( ( _om e. On /\ A e. _om /\ (/) e. A ) -> ( A .o _om ) = _om )