Metamath Proof Explorer

Theorem oaabs2

Description: The absorption law oaabs is also a property of higher powers of _om . (Contributed by Mario Carneiro, 29-May-2015)

Ref Expression
Assertion oaabs2 
|- ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( A +o B ) = B )

Proof

Step Hyp Ref Expression
1 n0i 
 |-  ( A e. ( _om ^o C ) -> -. ( _om ^o C ) = (/) )
2 fnoe 
 |-  ^o Fn ( On X. On )
3 fndm 
 |-  ( ^o Fn ( On X. On ) -> dom ^o = ( On X. On ) )
4 2 3 ax-mp 
 |-  dom ^o = ( On X. On )
5 4 ndmov 
 |-  ( -. ( _om e. On /\ C e. On ) -> ( _om ^o C ) = (/) )
6 1 5 nsyl2 
 |-  ( A e. ( _om ^o C ) -> ( _om e. On /\ C e. On ) )
7 6 ad2antrr 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( _om e. On /\ C e. On ) )
8 oecl 
 |-  ( ( _om e. On /\ C e. On ) -> ( _om ^o C ) e. On )
9 7 8 syl 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( _om ^o C ) e. On )
10 simplr 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> B e. On )
11 simpr 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( _om ^o C ) C_ B )
12 oawordeu 
 |-  ( ( ( ( _om ^o C ) e. On /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> E! x e. On ( ( _om ^o C ) +o x ) = B )
13 9 10 11 12 syl21anc 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> E! x e. On ( ( _om ^o C ) +o x ) = B )
14 reurex 
 |-  ( E! x e. On ( ( _om ^o C ) +o x ) = B -> E. x e. On ( ( _om ^o C ) +o x ) = B )
15 13 14 syl 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> E. x e. On ( ( _om ^o C ) +o x ) = B )
16 simpll 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> A e. ( _om ^o C ) )
17 onelon 
 |-  ( ( ( _om ^o C ) e. On /\ A e. ( _om ^o C ) ) -> A e. On )
18 9 16 17 syl2anc 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> A e. On )
19 18 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> A e. On )
20 9 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> ( _om ^o C ) e. On )
21 simpr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> x e. On )
22 oaass 
 |-  ( ( A e. On /\ ( _om ^o C ) e. On /\ x e. On ) -> ( ( A +o ( _om ^o C ) ) +o x ) = ( A +o ( ( _om ^o C ) +o x ) ) )
23 19 20 21 22 syl3anc 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> ( ( A +o ( _om ^o C ) ) +o x ) = ( A +o ( ( _om ^o C ) +o x ) ) )
24 7 simprd 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> C e. On )
25 eloni 
 |-  ( C e. On -> Ord C )
26 24 25 syl 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> Ord C )
27 ordzsl 
 |-  ( Ord C <-> ( C = (/) \/ E. x e. On C = suc x \/ Lim C ) )
28 26 27 sylib 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( C = (/) \/ E. x e. On C = suc x \/ Lim C ) )
29 simplll 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> A e. ( _om ^o C ) )
30 oveq2 
 |-  ( C = (/) -> ( _om ^o C ) = ( _om ^o (/) ) )
31 7 simpld 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> _om e. On )
32 oe0 
 |-  ( _om e. On -> ( _om ^o (/) ) = 1o )
33 31 32 syl 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( _om ^o (/) ) = 1o )
34 30 33 sylan9eqr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> ( _om ^o C ) = 1o )
35 29 34 eleqtrd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> A e. 1o )
36 el1o 
 |-  ( A e. 1o <-> A = (/) )
37 35 36 sylib 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> A = (/) )
38 37 oveq1d 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> ( A +o ( _om ^o C ) ) = ( (/) +o ( _om ^o C ) ) )
39 9 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> ( _om ^o C ) e. On )
40 oa0r 
 |-  ( ( _om ^o C ) e. On -> ( (/) +o ( _om ^o C ) ) = ( _om ^o C ) )
41 39 40 syl 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> ( (/) +o ( _om ^o C ) ) = ( _om ^o C ) )
42 38 41 eqtrd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ C = (/) ) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) )
43 42 ex 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( C = (/) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) ) )
44 31 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> _om e. On )
45 simprl 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> x e. On )
46 oecl 
 |-  ( ( _om e. On /\ x e. On ) -> ( _om ^o x ) e. On )
47 44 45 46 syl2anc 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( _om ^o x ) e. On )
48 limom 
 |-  Lim _om
49 44 48 jctir 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( _om e. On /\ Lim _om ) )
50 simplll 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> A e. ( _om ^o C ) )
51 simprr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> C = suc x )
52 51 oveq2d 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( _om ^o C ) = ( _om ^o suc x ) )
53 oesuc 
 |-  ( ( _om e. On /\ x e. On ) -> ( _om ^o suc x ) = ( ( _om ^o x ) .o _om ) )
54 44 45 53 syl2anc 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( _om ^o suc x ) = ( ( _om ^o x ) .o _om ) )
55 52 54 eqtrd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( _om ^o C ) = ( ( _om ^o x ) .o _om ) )
56 50 55 eleqtrd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> A e. ( ( _om ^o x ) .o _om ) )
57 omordlim 
 |-  ( ( ( ( _om ^o x ) e. On /\ ( _om e. On /\ Lim _om ) ) /\ A e. ( ( _om ^o x ) .o _om ) ) -> E. y e. _om A e. ( ( _om ^o x ) .o y ) )
58 47 49 56 57 syl21anc 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> E. y e. _om A e. ( ( _om ^o x ) .o y ) )
59 47 adantr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( _om ^o x ) e. On )
60 nnon 
 |-  ( y e. _om -> y e. On )
61 60 ad2antrl 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> y e. On )
62 omcl 
 |-  ( ( ( _om ^o x ) e. On /\ y e. On ) -> ( ( _om ^o x ) .o y ) e. On )
63 59 61 62 syl2anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( ( _om ^o x ) .o y ) e. On )
64 eloni 
 |-  ( ( ( _om ^o x ) .o y ) e. On -> Ord ( ( _om ^o x ) .o y ) )
65 63 64 syl 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> Ord ( ( _om ^o x ) .o y ) )
66 simprr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> A e. ( ( _om ^o x ) .o y ) )
67 ordelss 
 |-  ( ( Ord ( ( _om ^o x ) .o y ) /\ A e. ( ( _om ^o x ) .o y ) ) -> A C_ ( ( _om ^o x ) .o y ) )
68 65 66 67 syl2anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> A C_ ( ( _om ^o x ) .o y ) )
69 18 ad2antrr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> A e. On )
70 9 ad2antrr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( _om ^o C ) e. On )
71 oawordri 
 |-  ( ( A e. On /\ ( ( _om ^o x ) .o y ) e. On /\ ( _om ^o C ) e. On ) -> ( A C_ ( ( _om ^o x ) .o y ) -> ( A +o ( _om ^o C ) ) C_ ( ( ( _om ^o x ) .o y ) +o ( _om ^o C ) ) ) )
72 69 63 70 71 syl3anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( A C_ ( ( _om ^o x ) .o y ) -> ( A +o ( _om ^o C ) ) C_ ( ( ( _om ^o x ) .o y ) +o ( _om ^o C ) ) ) )
73 68 72 mpd 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( A +o ( _om ^o C ) ) C_ ( ( ( _om ^o x ) .o y ) +o ( _om ^o C ) ) )
74 44 adantr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> _om e. On )
75 odi 
 |-  ( ( ( _om ^o x ) e. On /\ y e. On /\ _om e. On ) -> ( ( _om ^o x ) .o ( y +o _om ) ) = ( ( ( _om ^o x ) .o y ) +o ( ( _om ^o x ) .o _om ) ) )
76 59 61 74 75 syl3anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( ( _om ^o x ) .o ( y +o _om ) ) = ( ( ( _om ^o x ) .o y ) +o ( ( _om ^o x ) .o _om ) ) )
77 simprl 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> y e. _om )
78 oaabslem 
 |-  ( ( _om e. On /\ y e. _om ) -> ( y +o _om ) = _om )
79 74 77 78 syl2anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( y +o _om ) = _om )
80 79 oveq2d 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( ( _om ^o x ) .o ( y +o _om ) ) = ( ( _om ^o x ) .o _om ) )
81 76 80 eqtr3d 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( ( ( _om ^o x ) .o y ) +o ( ( _om ^o x ) .o _om ) ) = ( ( _om ^o x ) .o _om ) )
82 55 adantr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( _om ^o C ) = ( ( _om ^o x ) .o _om ) )
83 82 oveq2d 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( ( ( _om ^o x ) .o y ) +o ( _om ^o C ) ) = ( ( ( _om ^o x ) .o y ) +o ( ( _om ^o x ) .o _om ) ) )
84 81 83 82 3eqtr4d 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( ( ( _om ^o x ) .o y ) +o ( _om ^o C ) ) = ( _om ^o C ) )
85 73 84 sseqtrd 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) /\ ( y e. _om /\ A e. ( ( _om ^o x ) .o y ) ) ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) )
86 58 85 rexlimddv 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) )
87 oaword2 
 |-  ( ( ( _om ^o C ) e. On /\ A e. On ) -> ( _om ^o C ) C_ ( A +o ( _om ^o C ) ) )
88 9 18 87 syl2anc 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( _om ^o C ) C_ ( A +o ( _om ^o C ) ) )
89 88 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( _om ^o C ) C_ ( A +o ( _om ^o C ) ) )
90 86 89 eqssd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ ( x e. On /\ C = suc x ) ) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) )
91 90 rexlimdvaa 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( E. x e. On C = suc x -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) ) )
92 simplll 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> A e. ( _om ^o C ) )
93 31 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> _om e. On )
94 24 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> C e. On )
95 simpr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> Lim C )
96 oelim2 
 |-  ( ( _om e. On /\ ( C e. On /\ Lim C ) ) -> ( _om ^o C ) = U_ x e. ( C \ 1o ) ( _om ^o x ) )
97 93 94 95 96 syl12anc 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( _om ^o C ) = U_ x e. ( C \ 1o ) ( _om ^o x ) )
98 92 97 eleqtrd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> A e. U_ x e. ( C \ 1o ) ( _om ^o x ) )
99 eliun 
 |-  ( A e. U_ x e. ( C \ 1o ) ( _om ^o x ) <-> E. x e. ( C \ 1o ) A e. ( _om ^o x ) )
100 98 99 sylib 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> E. x e. ( C \ 1o ) A e. ( _om ^o x ) )
101 eldifi 
 |-  ( x e. ( C \ 1o ) -> x e. C )
102 18 ad2antrr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> A e. On )
103 9 ad2antrr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> ( _om ^o C ) e. On )
104 93 adantr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> _om e. On )
105 1onn 
 |-  1o e. _om
106 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
107 104 105 106 sylanblrc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> _om e. ( On \ 2o ) )
108 94 adantr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> C e. On )
109 simplr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> Lim C )
110 oelimcl 
 |-  ( ( _om e. ( On \ 2o ) /\ ( C e. On /\ Lim C ) ) -> Lim ( _om ^o C ) )
111 107 108 109 110 syl12anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> Lim ( _om ^o C ) )
112 oalim 
 |-  ( ( A e. On /\ ( ( _om ^o C ) e. On /\ Lim ( _om ^o C ) ) ) -> ( A +o ( _om ^o C ) ) = U_ y e. ( _om ^o C ) ( A +o y ) )
113 102 103 111 112 syl12anc 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> ( A +o ( _om ^o C ) ) = U_ y e. ( _om ^o C ) ( A +o y ) )
114 oelim2 
 |-  ( ( _om e. On /\ ( C e. On /\ Lim C ) ) -> ( _om ^o C ) = U_ z e. ( C \ 1o ) ( _om ^o z ) )
115 93 94 95 114 syl12anc 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( _om ^o C ) = U_ z e. ( C \ 1o ) ( _om ^o z ) )
116 115 eleq2d 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( y e. ( _om ^o C ) <-> y e. U_ z e. ( C \ 1o ) ( _om ^o z ) ) )
117 eliun 
 |-  ( y e. U_ z e. ( C \ 1o ) ( _om ^o z ) <-> E. z e. ( C \ 1o ) y e. ( _om ^o z ) )
118 116 117 bitrdi 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( y e. ( _om ^o C ) <-> E. z e. ( C \ 1o ) y e. ( _om ^o z ) ) )
119 118 adantr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> ( y e. ( _om ^o C ) <-> E. z e. ( C \ 1o ) y e. ( _om ^o z ) ) )
120 eldifi 
 |-  ( z e. ( C \ 1o ) -> z e. C )
121 104 adantr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> _om e. On )
122 108 adantr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> C e. On )
123 simplrl 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> x e. C )
124 onelon 
 |-  ( ( C e. On /\ x e. C ) -> x e. On )
125 122 123 124 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> x e. On )
126 121 125 46 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o x ) e. On )
127 eloni 
 |-  ( ( _om ^o x ) e. On -> Ord ( _om ^o x ) )
128 126 127 syl 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> Ord ( _om ^o x ) )
129 simplrr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> A e. ( _om ^o x ) )
130 ordelss 
 |-  ( ( Ord ( _om ^o x ) /\ A e. ( _om ^o x ) ) -> A C_ ( _om ^o x ) )
131 128 129 130 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> A C_ ( _om ^o x ) )
132 ssun1 
 |-  x C_ ( x u. z )
133 26 ad3antrrr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> Ord C )
134 simprl 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> z e. C )
135 ordunel 
 |-  ( ( Ord C /\ x e. C /\ z e. C ) -> ( x u. z ) e. C )
136 133 123 134 135 syl3anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( x u. z ) e. C )
137 onelon 
 |-  ( ( C e. On /\ ( x u. z ) e. C ) -> ( x u. z ) e. On )
138 122 136 137 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( x u. z ) e. On )
139 peano1 
 |-  (/) e. _om
140 139 a1i 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> (/) e. _om )
141 oewordi 
 |-  ( ( ( x e. On /\ ( x u. z ) e. On /\ _om e. On ) /\ (/) e. _om ) -> ( x C_ ( x u. z ) -> ( _om ^o x ) C_ ( _om ^o ( x u. z ) ) ) )
142 125 138 121 140 141 syl31anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( x C_ ( x u. z ) -> ( _om ^o x ) C_ ( _om ^o ( x u. z ) ) ) )
143 132 142 mpi 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o x ) C_ ( _om ^o ( x u. z ) ) )
144 131 143 sstrd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> A C_ ( _om ^o ( x u. z ) ) )
145 102 adantr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> A e. On )
146 oecl 
 |-  ( ( _om e. On /\ ( x u. z ) e. On ) -> ( _om ^o ( x u. z ) ) e. On )
147 121 138 146 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o ( x u. z ) ) e. On )
148 onelon 
 |-  ( ( C e. On /\ z e. C ) -> z e. On )
149 122 134 148 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> z e. On )
150 oecl 
 |-  ( ( _om e. On /\ z e. On ) -> ( _om ^o z ) e. On )
151 121 149 150 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o z ) e. On )
152 simprr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> y e. ( _om ^o z ) )
153 onelon 
 |-  ( ( ( _om ^o z ) e. On /\ y e. ( _om ^o z ) ) -> y e. On )
154 151 152 153 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> y e. On )
155 oawordri 
 |-  ( ( A e. On /\ ( _om ^o ( x u. z ) ) e. On /\ y e. On ) -> ( A C_ ( _om ^o ( x u. z ) ) -> ( A +o y ) C_ ( ( _om ^o ( x u. z ) ) +o y ) ) )
156 145 147 154 155 syl3anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( A C_ ( _om ^o ( x u. z ) ) -> ( A +o y ) C_ ( ( _om ^o ( x u. z ) ) +o y ) ) )
157 144 156 mpd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( A +o y ) C_ ( ( _om ^o ( x u. z ) ) +o y ) )
158 eloni 
 |-  ( ( _om ^o z ) e. On -> Ord ( _om ^o z ) )
159 151 158 syl 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> Ord ( _om ^o z ) )
160 ordelss 
 |-  ( ( Ord ( _om ^o z ) /\ y e. ( _om ^o z ) ) -> y C_ ( _om ^o z ) )
161 159 152 160 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> y C_ ( _om ^o z ) )
162 ssun2 
 |-  z C_ ( x u. z )
163 oewordi 
 |-  ( ( ( z e. On /\ ( x u. z ) e. On /\ _om e. On ) /\ (/) e. _om ) -> ( z C_ ( x u. z ) -> ( _om ^o z ) C_ ( _om ^o ( x u. z ) ) ) )
164 149 138 121 140 163 syl31anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( z C_ ( x u. z ) -> ( _om ^o z ) C_ ( _om ^o ( x u. z ) ) ) )
165 162 164 mpi 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o z ) C_ ( _om ^o ( x u. z ) ) )
166 161 165 sstrd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> y C_ ( _om ^o ( x u. z ) ) )
167 oaword 
 |-  ( ( y e. On /\ ( _om ^o ( x u. z ) ) e. On /\ ( _om ^o ( x u. z ) ) e. On ) -> ( y C_ ( _om ^o ( x u. z ) ) <-> ( ( _om ^o ( x u. z ) ) +o y ) C_ ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) ) )
168 154 147 147 167 syl3anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( y C_ ( _om ^o ( x u. z ) ) <-> ( ( _om ^o ( x u. z ) ) +o y ) C_ ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) ) )
169 166 168 mpbid 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( _om ^o ( x u. z ) ) +o y ) C_ ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) )
170 157 169 sstrd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( A +o y ) C_ ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) )
171 ordom 
 |-  Ord _om
172 ordsucss 
 |-  ( Ord _om -> ( 1o e. _om -> suc 1o C_ _om ) )
173 171 105 172 mp2 
 |-  suc 1o C_ _om
174 1on 
 |-  1o e. On
175 suceloni 
 |-  ( 1o e. On -> suc 1o e. On )
176 174 175 mp1i 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> suc 1o e. On )
177 omwordi 
 |-  ( ( suc 1o e. On /\ _om e. On /\ ( _om ^o ( x u. z ) ) e. On ) -> ( suc 1o C_ _om -> ( ( _om ^o ( x u. z ) ) .o suc 1o ) C_ ( ( _om ^o ( x u. z ) ) .o _om ) ) )
178 176 121 147 177 syl3anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( suc 1o C_ _om -> ( ( _om ^o ( x u. z ) ) .o suc 1o ) C_ ( ( _om ^o ( x u. z ) ) .o _om ) ) )
179 173 178 mpi 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( _om ^o ( x u. z ) ) .o suc 1o ) C_ ( ( _om ^o ( x u. z ) ) .o _om ) )
180 174 a1i 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> 1o e. On )
181 omsuc 
 |-  ( ( ( _om ^o ( x u. z ) ) e. On /\ 1o e. On ) -> ( ( _om ^o ( x u. z ) ) .o suc 1o ) = ( ( ( _om ^o ( x u. z ) ) .o 1o ) +o ( _om ^o ( x u. z ) ) ) )
182 147 180 181 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( _om ^o ( x u. z ) ) .o suc 1o ) = ( ( ( _om ^o ( x u. z ) ) .o 1o ) +o ( _om ^o ( x u. z ) ) ) )
183 om1 
 |-  ( ( _om ^o ( x u. z ) ) e. On -> ( ( _om ^o ( x u. z ) ) .o 1o ) = ( _om ^o ( x u. z ) ) )
184 147 183 syl 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( _om ^o ( x u. z ) ) .o 1o ) = ( _om ^o ( x u. z ) ) )
185 184 oveq1d 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( ( _om ^o ( x u. z ) ) .o 1o ) +o ( _om ^o ( x u. z ) ) ) = ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) )
186 182 185 eqtr2d 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) = ( ( _om ^o ( x u. z ) ) .o suc 1o ) )
187 oesuc 
 |-  ( ( _om e. On /\ ( x u. z ) e. On ) -> ( _om ^o suc ( x u. z ) ) = ( ( _om ^o ( x u. z ) ) .o _om ) )
188 121 138 187 syl2anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o suc ( x u. z ) ) = ( ( _om ^o ( x u. z ) ) .o _om ) )
189 179 186 188 3sstr4d 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( ( _om ^o ( x u. z ) ) +o ( _om ^o ( x u. z ) ) ) C_ ( _om ^o suc ( x u. z ) ) )
190 170 189 sstrd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( A +o y ) C_ ( _om ^o suc ( x u. z ) ) )
191 ordsucss 
 |-  ( Ord C -> ( ( x u. z ) e. C -> suc ( x u. z ) C_ C ) )
192 133 136 191 sylc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> suc ( x u. z ) C_ C )
193 suceloni 
 |-  ( ( x u. z ) e. On -> suc ( x u. z ) e. On )
194 138 193 syl 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> suc ( x u. z ) e. On )
195 oewordi 
 |-  ( ( ( suc ( x u. z ) e. On /\ C e. On /\ _om e. On ) /\ (/) e. _om ) -> ( suc ( x u. z ) C_ C -> ( _om ^o suc ( x u. z ) ) C_ ( _om ^o C ) ) )
196 194 122 121 140 195 syl31anc 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( suc ( x u. z ) C_ C -> ( _om ^o suc ( x u. z ) ) C_ ( _om ^o C ) ) )
197 192 196 mpd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( _om ^o suc ( x u. z ) ) C_ ( _om ^o C ) )
198 190 197 sstrd 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ ( z e. C /\ y e. ( _om ^o z ) ) ) -> ( A +o y ) C_ ( _om ^o C ) )
199 198 expr 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ z e. C ) -> ( y e. ( _om ^o z ) -> ( A +o y ) C_ ( _om ^o C ) ) )
200 120 199 sylan2 
 |-  ( ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) /\ z e. ( C \ 1o ) ) -> ( y e. ( _om ^o z ) -> ( A +o y ) C_ ( _om ^o C ) ) )
201 200 rexlimdva 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> ( E. z e. ( C \ 1o ) y e. ( _om ^o z ) -> ( A +o y ) C_ ( _om ^o C ) ) )
202 119 201 sylbid 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> ( y e. ( _om ^o C ) -> ( A +o y ) C_ ( _om ^o C ) ) )
203 202 ralrimiv 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> A. y e. ( _om ^o C ) ( A +o y ) C_ ( _om ^o C ) )
204 iunss 
 |-  ( U_ y e. ( _om ^o C ) ( A +o y ) C_ ( _om ^o C ) <-> A. y e. ( _om ^o C ) ( A +o y ) C_ ( _om ^o C ) )
205 203 204 sylibr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> U_ y e. ( _om ^o C ) ( A +o y ) C_ ( _om ^o C ) )
206 113 205 eqsstrd 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ ( x e. C /\ A e. ( _om ^o x ) ) ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) )
207 206 expr 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ x e. C ) -> ( A e. ( _om ^o x ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) ) )
208 101 207 sylan2 
 |-  ( ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) /\ x e. ( C \ 1o ) ) -> ( A e. ( _om ^o x ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) ) )
209 208 rexlimdva 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( E. x e. ( C \ 1o ) A e. ( _om ^o x ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) ) )
210 100 209 mpd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( A +o ( _om ^o C ) ) C_ ( _om ^o C ) )
211 88 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( _om ^o C ) C_ ( A +o ( _om ^o C ) ) )
212 210 211 eqssd 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ Lim C ) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) )
213 212 ex 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( Lim C -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) ) )
214 43 91 213 3jaod 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( ( C = (/) \/ E. x e. On C = suc x \/ Lim C ) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) ) )
215 28 214 mpd 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) )
216 215 adantr 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> ( A +o ( _om ^o C ) ) = ( _om ^o C ) )
217 216 oveq1d 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> ( ( A +o ( _om ^o C ) ) +o x ) = ( ( _om ^o C ) +o x ) )
218 23 217 eqtr3d 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> ( A +o ( ( _om ^o C ) +o x ) ) = ( ( _om ^o C ) +o x ) )
219 oveq2 
 |-  ( ( ( _om ^o C ) +o x ) = B -> ( A +o ( ( _om ^o C ) +o x ) ) = ( A +o B ) )
220 id 
 |-  ( ( ( _om ^o C ) +o x ) = B -> ( ( _om ^o C ) +o x ) = B )
221 219 220 eqeq12d 
 |-  ( ( ( _om ^o C ) +o x ) = B -> ( ( A +o ( ( _om ^o C ) +o x ) ) = ( ( _om ^o C ) +o x ) <-> ( A +o B ) = B ) )
222 218 221 syl5ibcom 
 |-  ( ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) /\ x e. On ) -> ( ( ( _om ^o C ) +o x ) = B -> ( A +o B ) = B ) )
223 222 rexlimdva 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( E. x e. On ( ( _om ^o C ) +o x ) = B -> ( A +o B ) = B ) )
224 15 223 mpd 
 |-  ( ( ( A e. ( _om ^o C ) /\ B e. On ) /\ ( _om ^o C ) C_ B ) -> ( A +o B ) = B )