Metamath Proof Explorer

Theorem omabs

Description: Ordinal multiplication is also absorbed by powers of _om . (Contributed by Mario Carneiro, 30-May-2015)

Ref Expression
Assertion omabs 
|- ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = (/) -> ( (/) e. x <-> (/) e. (/) ) )
2 oveq2 
 |-  ( x = (/) -> ( _om ^o x ) = ( _om ^o (/) ) )
3 2 oveq2d 
 |-  ( x = (/) -> ( A .o ( _om ^o x ) ) = ( A .o ( _om ^o (/) ) ) )
4 3 2 eqeq12d 
 |-  ( x = (/) -> ( ( A .o ( _om ^o x ) ) = ( _om ^o x ) <-> ( A .o ( _om ^o (/) ) ) = ( _om ^o (/) ) ) )
5 1 4 imbi12d 
 |-  ( x = (/) -> ( ( (/) e. x -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) <-> ( (/) e. (/) -> ( A .o ( _om ^o (/) ) ) = ( _om ^o (/) ) ) ) )
6 eleq2 
 |-  ( x = y -> ( (/) e. x <-> (/) e. y ) )
7 oveq2 
 |-  ( x = y -> ( _om ^o x ) = ( _om ^o y ) )
8 7 oveq2d 
 |-  ( x = y -> ( A .o ( _om ^o x ) ) = ( A .o ( _om ^o y ) ) )
9 8 7 eqeq12d 
 |-  ( x = y -> ( ( A .o ( _om ^o x ) ) = ( _om ^o x ) <-> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) )
10 6 9 imbi12d 
 |-  ( x = y -> ( ( (/) e. x -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) <-> ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) )
11 eleq2 
 |-  ( x = suc y -> ( (/) e. x <-> (/) e. suc y ) )
12 oveq2 
 |-  ( x = suc y -> ( _om ^o x ) = ( _om ^o suc y ) )
13 12 oveq2d 
 |-  ( x = suc y -> ( A .o ( _om ^o x ) ) = ( A .o ( _om ^o suc y ) ) )
14 13 12 eqeq12d 
 |-  ( x = suc y -> ( ( A .o ( _om ^o x ) ) = ( _om ^o x ) <-> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) )
15 11 14 imbi12d 
 |-  ( x = suc y -> ( ( (/) e. x -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) <-> ( (/) e. suc y -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) )
16 eleq2 
 |-  ( x = B -> ( (/) e. x <-> (/) e. B ) )
17 oveq2 
 |-  ( x = B -> ( _om ^o x ) = ( _om ^o B ) )
18 17 oveq2d 
 |-  ( x = B -> ( A .o ( _om ^o x ) ) = ( A .o ( _om ^o B ) ) )
19 18 17 eqeq12d 
 |-  ( x = B -> ( ( A .o ( _om ^o x ) ) = ( _om ^o x ) <-> ( A .o ( _om ^o B ) ) = ( _om ^o B ) ) )
20 16 19 imbi12d 
 |-  ( x = B -> ( ( (/) e. x -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) <-> ( (/) e. B -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) ) ) )
21 noel 
 |-  -. (/) e. (/)
22 21 pm2.21i 
 |-  ( (/) e. (/) -> ( A .o ( _om ^o (/) ) ) = ( _om ^o (/) ) )
23 22 a1i 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) -> ( (/) e. (/) -> ( A .o ( _om ^o (/) ) ) = ( _om ^o (/) ) ) )
24 simprl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> _om e. On )
25 simpll 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> A e. _om )
26 simplr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> (/) e. A )
27 omabslem 
 |-  ( ( _om e. On /\ A e. _om /\ (/) e. A ) -> ( A .o _om ) = _om )
28 24 25 26 27 syl3anc 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( A .o _om ) = _om )
29 28 adantr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) /\ y = (/) ) -> ( A .o _om ) = _om )
30 suceq 
 |-  ( y = (/) -> suc y = suc (/) )
31 df-1o 
 |-  1o = suc (/)
32 30 31 eqtr4di 
 |-  ( y = (/) -> suc y = 1o )
33 32 oveq2d 
 |-  ( y = (/) -> ( _om ^o suc y ) = ( _om ^o 1o ) )
34 oe1 
 |-  ( _om e. On -> ( _om ^o 1o ) = _om )
35 34 ad2antrl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( _om ^o 1o ) = _om )
36 33 35 sylan9eqr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) /\ y = (/) ) -> ( _om ^o suc y ) = _om )
37 36 oveq2d 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) /\ y = (/) ) -> ( A .o ( _om ^o suc y ) ) = ( A .o _om ) )
38 29 37 36 3eqtr4d 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) /\ y = (/) ) -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) )
39 38 ex 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( y = (/) -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) )
40 39 a1dd 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( y = (/) -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) )
41 oveq1 
 |-  ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) -> ( ( A .o ( _om ^o y ) ) .o _om ) = ( ( _om ^o y ) .o _om ) )
42 oesuc 
 |-  ( ( _om e. On /\ y e. On ) -> ( _om ^o suc y ) = ( ( _om ^o y ) .o _om ) )
43 42 adantl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( _om ^o suc y ) = ( ( _om ^o y ) .o _om ) )
44 43 oveq2d 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( A .o ( _om ^o suc y ) ) = ( A .o ( ( _om ^o y ) .o _om ) ) )
45 nnon 
 |-  ( A e. _om -> A e. On )
46 45 ad2antrr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> A e. On )
47 oecl 
 |-  ( ( _om e. On /\ y e. On ) -> ( _om ^o y ) e. On )
48 47 adantl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( _om ^o y ) e. On )
49 omass 
 |-  ( ( A e. On /\ ( _om ^o y ) e. On /\ _om e. On ) -> ( ( A .o ( _om ^o y ) ) .o _om ) = ( A .o ( ( _om ^o y ) .o _om ) ) )
50 46 48 24 49 syl3anc 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( ( A .o ( _om ^o y ) ) .o _om ) = ( A .o ( ( _om ^o y ) .o _om ) ) )
51 44 50 eqtr4d 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( A .o ( _om ^o suc y ) ) = ( ( A .o ( _om ^o y ) ) .o _om ) )
52 51 43 eqeq12d 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) <-> ( ( A .o ( _om ^o y ) ) .o _om ) = ( ( _om ^o y ) .o _om ) ) )
53 41 52 imbitrrid 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) )
54 53 imim2d 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. y -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) )
55 54 com23 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( (/) e. y -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) )
56 simprr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> y e. On )
57 on0eqel 
 |-  ( y e. On -> ( y = (/) \/ (/) e. y ) )
58 56 57 syl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( y = (/) \/ (/) e. y ) )
59 40 55 58 mpjaod 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) )
60 59 a1dd 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ y e. On ) ) -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. suc y -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) )
61 60 anassrs 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) /\ y e. On ) -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. suc y -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) )
62 61 expcom 
 |-  ( y e. On -> ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) -> ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. suc y -> ( A .o ( _om ^o suc y ) ) = ( _om ^o suc y ) ) ) ) )
63 45 ad3antrrr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> A e. On )
64 simprl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> _om e. On )
65 simprr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> Lim x )
66 vex 
 |-  x e. _V
67 65 66 jctil 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> ( x e. _V /\ Lim x ) )
68 limelon 
 |-  ( ( x e. _V /\ Lim x ) -> x e. On )
69 67 68 syl 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> x e. On )
70 oecl 
 |-  ( ( _om e. On /\ x e. On ) -> ( _om ^o x ) e. On )
71 64 69 70 syl2anc 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> ( _om ^o x ) e. On )
72 71 adantr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( _om ^o x ) e. On )
73 1onn 
 |-  1o e. _om
74 ondif2 
 |-  ( _om e. ( On \ 2o ) <-> ( _om e. On /\ 1o e. _om ) )
75 64 73 74 sylanblrc 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> _om e. ( On \ 2o ) )
76 75 adantr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> _om e. ( On \ 2o ) )
77 67 adantr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( x e. _V /\ Lim x ) )
78 oelimcl 
 |-  ( ( _om e. ( On \ 2o ) /\ ( x e. _V /\ Lim x ) ) -> Lim ( _om ^o x ) )
79 76 77 78 syl2anc 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> Lim ( _om ^o x ) )
80 omlim 
 |-  ( ( A e. On /\ ( ( _om ^o x ) e. On /\ Lim ( _om ^o x ) ) ) -> ( A .o ( _om ^o x ) ) = U_ z e. ( _om ^o x ) ( A .o z ) )
81 63 72 79 80 syl12anc 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( A .o ( _om ^o x ) ) = U_ z e. ( _om ^o x ) ( A .o z ) )
82 simplrl 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> _om e. On )
83 oelim2 
 |-  ( ( _om e. On /\ ( x e. _V /\ Lim x ) ) -> ( _om ^o x ) = U_ y e. ( x \ 1o ) ( _om ^o y ) )
84 82 77 83 syl2anc 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( _om ^o x ) = U_ y e. ( x \ 1o ) ( _om ^o y ) )
85 84 eleq2d 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( z e. ( _om ^o x ) <-> z e. U_ y e. ( x \ 1o ) ( _om ^o y ) ) )
86 eliun 
 |-  ( z e. U_ y e. ( x \ 1o ) ( _om ^o y ) <-> E. y e. ( x \ 1o ) z e. ( _om ^o y ) )
87 85 86 bitrdi 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( z e. ( _om ^o x ) <-> E. y e. ( x \ 1o ) z e. ( _om ^o y ) ) )
88 69 adantr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> x e. On )
89 anass 
 |-  ( ( ( y e. x /\ (/) e. y ) /\ z e. ( _om ^o y ) ) <-> ( y e. x /\ ( (/) e. y /\ z e. ( _om ^o y ) ) ) )
90 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
91 on0eln0 
 |-  ( y e. On -> ( (/) e. y <-> y =/= (/) ) )
92 90 91 syl 
 |-  ( ( x e. On /\ y e. x ) -> ( (/) e. y <-> y =/= (/) ) )
93 92 pm5.32da 
 |-  ( x e. On -> ( ( y e. x /\ (/) e. y ) <-> ( y e. x /\ y =/= (/) ) ) )
94 dif1o 
 |-  ( y e. ( x \ 1o ) <-> ( y e. x /\ y =/= (/) ) )
95 93 94 bitr4di 
 |-  ( x e. On -> ( ( y e. x /\ (/) e. y ) <-> y e. ( x \ 1o ) ) )
96 95 anbi1d 
 |-  ( x e. On -> ( ( ( y e. x /\ (/) e. y ) /\ z e. ( _om ^o y ) ) <-> ( y e. ( x \ 1o ) /\ z e. ( _om ^o y ) ) ) )
97 89 96 bitr3id 
 |-  ( x e. On -> ( ( y e. x /\ ( (/) e. y /\ z e. ( _om ^o y ) ) ) <-> ( y e. ( x \ 1o ) /\ z e. ( _om ^o y ) ) ) )
98 97 rexbidv2 
 |-  ( x e. On -> ( E. y e. x ( (/) e. y /\ z e. ( _om ^o y ) ) <-> E. y e. ( x \ 1o ) z e. ( _om ^o y ) ) )
99 88 98 syl 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( E. y e. x ( (/) e. y /\ z e. ( _om ^o y ) ) <-> E. y e. ( x \ 1o ) z e. ( _om ^o y ) ) )
100 87 99 bitr4d 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( z e. ( _om ^o x ) <-> E. y e. x ( (/) e. y /\ z e. ( _om ^o y ) ) ) )
101 r19.29 
 |-  ( ( A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ E. y e. x ( (/) e. y /\ z e. ( _om ^o y ) ) ) -> E. y e. x ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ ( (/) e. y /\ z e. ( _om ^o y ) ) ) )
102 id 
 |-  ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) )
103 102 imp 
 |-  ( ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ (/) e. y ) -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) )
104 103 anim1i 
 |-  ( ( ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ (/) e. y ) /\ z e. ( _om ^o y ) ) -> ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) )
105 104 anasss 
 |-  ( ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ ( (/) e. y /\ z e. ( _om ^o y ) ) ) -> ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) )
106 71 ad2antrr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( _om ^o x ) e. On )
107 eloni 
 |-  ( ( _om ^o x ) e. On -> Ord ( _om ^o x ) )
108 106 107 syl 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> Ord ( _om ^o x ) )
109 simprr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> z e. ( _om ^o y ) )
110 64 ad2antrr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> _om e. On )
111 69 ad2antrr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> x e. On )
112 simplr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> y e. x )
113 111 112 90 syl2anc 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> y e. On )
114 110 113 47 syl2anc 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( _om ^o y ) e. On )
115 onelon 
 |-  ( ( ( _om ^o y ) e. On /\ z e. ( _om ^o y ) ) -> z e. On )
116 114 109 115 syl2anc 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> z e. On )
117 45 ad2antrr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> A e. On )
118 117 ad2antrr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> A e. On )
119 simplr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> (/) e. A )
120 119 ad2antrr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> (/) e. A )
121 omord2 
 |-  ( ( ( z e. On /\ ( _om ^o y ) e. On /\ A e. On ) /\ (/) e. A ) -> ( z e. ( _om ^o y ) <-> ( A .o z ) e. ( A .o ( _om ^o y ) ) ) )
122 116 114 118 120 121 syl31anc 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( z e. ( _om ^o y ) <-> ( A .o z ) e. ( A .o ( _om ^o y ) ) ) )
123 109 122 mpbid 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) e. ( A .o ( _om ^o y ) ) )
124 simprl 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) )
125 123 124 eleqtrd 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) e. ( _om ^o y ) )
126 75 ad2antrr 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> _om e. ( On \ 2o ) )
127 oeord 
 |-  ( ( y e. On /\ x e. On /\ _om e. ( On \ 2o ) ) -> ( y e. x <-> ( _om ^o y ) e. ( _om ^o x ) ) )
128 113 111 126 127 syl3anc 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( y e. x <-> ( _om ^o y ) e. ( _om ^o x ) ) )
129 112 128 mpbid 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( _om ^o y ) e. ( _om ^o x ) )
130 ontr1 
 |-  ( ( _om ^o x ) e. On -> ( ( ( A .o z ) e. ( _om ^o y ) /\ ( _om ^o y ) e. ( _om ^o x ) ) -> ( A .o z ) e. ( _om ^o x ) ) )
131 106 130 syl 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( ( ( A .o z ) e. ( _om ^o y ) /\ ( _om ^o y ) e. ( _om ^o x ) ) -> ( A .o z ) e. ( _om ^o x ) ) )
132 125 129 131 mp2and 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) e. ( _om ^o x ) )
133 ordelss 
 |-  ( ( Ord ( _om ^o x ) /\ ( A .o z ) e. ( _om ^o x ) ) -> ( A .o z ) C_ ( _om ^o x ) )
134 108 132 133 syl2anc 
 |-  ( ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) /\ ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) C_ ( _om ^o x ) )
135 134 ex 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) -> ( ( ( A .o ( _om ^o y ) ) = ( _om ^o y ) /\ z e. ( _om ^o y ) ) -> ( A .o z ) C_ ( _om ^o x ) ) )
136 105 135 syl5 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ y e. x ) -> ( ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ ( (/) e. y /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) C_ ( _om ^o x ) ) )
137 136 rexlimdva 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> ( E. y e. x ( ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ ( (/) e. y /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) C_ ( _om ^o x ) ) )
138 101 137 syl5 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> ( ( A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) /\ E. y e. x ( (/) e. y /\ z e. ( _om ^o y ) ) ) -> ( A .o z ) C_ ( _om ^o x ) ) )
139 138 expdimp 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( E. y e. x ( (/) e. y /\ z e. ( _om ^o y ) ) -> ( A .o z ) C_ ( _om ^o x ) ) )
140 100 139 sylbid 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( z e. ( _om ^o x ) -> ( A .o z ) C_ ( _om ^o x ) ) )
141 140 ralrimiv 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> A. z e. ( _om ^o x ) ( A .o z ) C_ ( _om ^o x ) )
142 iunss 
 |-  ( U_ z e. ( _om ^o x ) ( A .o z ) C_ ( _om ^o x ) <-> A. z e. ( _om ^o x ) ( A .o z ) C_ ( _om ^o x ) )
143 141 142 sylibr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> U_ z e. ( _om ^o x ) ( A .o z ) C_ ( _om ^o x ) )
144 81 143 eqsstrd 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( A .o ( _om ^o x ) ) C_ ( _om ^o x ) )
145 simpllr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> (/) e. A )
146 omword2 
 |-  ( ( ( ( _om ^o x ) e. On /\ A e. On ) /\ (/) e. A ) -> ( _om ^o x ) C_ ( A .o ( _om ^o x ) ) )
147 72 63 145 146 syl21anc 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( _om ^o x ) C_ ( A .o ( _om ^o x ) ) )
148 144 147 eqssd 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) /\ A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) ) -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) )
149 148 ex 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ Lim x ) ) -> ( A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) )
150 149 anassrs 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) /\ Lim x ) -> ( A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) )
151 150 a1dd 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) /\ Lim x ) -> ( A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. x -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) ) )
152 151 expcom 
 |-  ( Lim x -> ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) -> ( A. y e. x ( (/) e. y -> ( A .o ( _om ^o y ) ) = ( _om ^o y ) ) -> ( (/) e. x -> ( A .o ( _om ^o x ) ) = ( _om ^o x ) ) ) ) )
153 5 10 15 20 23 62 152 tfinds3 
 |-  ( B e. On -> ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) -> ( (/) e. B -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) ) ) )
154 153 com12 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ _om e. On ) -> ( B e. On -> ( (/) e. B -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) ) ) )
155 154 adantrr 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ B e. On ) ) -> ( B e. On -> ( (/) e. B -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) ) ) )
156 155 imp32 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( _om e. On /\ B e. On ) ) /\ ( B e. On /\ (/) e. B ) ) -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) )
157 156 an32s 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) /\ ( _om e. On /\ B e. On ) ) -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) )
158 nnm0 
 |-  ( A e. _om -> ( A .o (/) ) = (/) )
159 158 ad3antrrr 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) /\ -. ( _om e. On /\ B e. On ) ) -> ( A .o (/) ) = (/) )
160 fnoe 
 |-  ^o Fn ( On X. On )
161 fndm 
 |-  ( ^o Fn ( On X. On ) -> dom ^o = ( On X. On ) )
162 160 161 ax-mp 
 |-  dom ^o = ( On X. On )
163 162 ndmov 
 |-  ( -. ( _om e. On /\ B e. On ) -> ( _om ^o B ) = (/) )
164 163 adantl 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) /\ -. ( _om e. On /\ B e. On ) ) -> ( _om ^o B ) = (/) )
165 164 oveq2d 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) /\ -. ( _om e. On /\ B e. On ) ) -> ( A .o ( _om ^o B ) ) = ( A .o (/) ) )
166 159 165 164 3eqtr4d 
 |-  ( ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) /\ -. ( _om e. On /\ B e. On ) ) -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) )
167 157 166 pm2.61dan 
 |-  ( ( ( A e. _om /\ (/) e. A ) /\ ( B e. On /\ (/) e. B ) ) -> ( A .o ( _om ^o B ) ) = ( _om ^o B ) )