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 syl5ibr
 |-  ( ( ( 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 ) )