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

Metamath Proof Explorer

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 )