MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oaabs2 Unicode version

Theorem oaabs2 7313
Description: The absorption law oaabs 7312 is also a property of higher powers of . (Contributed by Mario Carneiro, 29-May-2015.)
Assertion
Ref Expression
oaabs2

Proof of Theorem oaabs2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 n0i 3789 . . . . . . 7
2 fnoe 7179 . . . . . . . . 9
3 fndm 5685 . . . . . . . . 9
42, 3ax-mp 5 . . . . . . . 8
54ndmov 6459 . . . . . . 7
61, 5nsyl2 127 . . . . . 6
76ad2antrr 725 . . . . 5
8 oecl 7206 . . . . 5
97, 8syl 16 . . . 4
10 simplr 755 . . . 4
11 simpr 461 . . . 4
12 oawordeu 7223 . . . 4
139, 10, 11, 12syl21anc 1227 . . 3
14 reurex 3074 . . 3
1513, 14syl 16 . 2
16 simpll 753 . . . . . . . 8
17 onelon 4908 . . . . . . . 8
189, 16, 17syl2anc 661 . . . . . . 7
1918adantr 465 . . . . . 6
209adantr 465 . . . . . 6
21 simpr 461 . . . . . 6
22 oaass 7229 . . . . . 6
2319, 20, 21, 22syl3anc 1228 . . . . 5
247simprd 463 . . . . . . . . . 10
25 eloni 4893 . . . . . . . . . 10
2624, 25syl 16 . . . . . . . . 9
27 ordzsl 6680 . . . . . . . . 9
2826, 27sylib 196 . . . . . . . 8
29 simplll 759 . . . . . . . . . . . . . 14
30 oveq2 6304 . . . . . . . . . . . . . . 15
317simpld 459 . . . . . . . . . . . . . . . 16
32 oe0 7191 . . . . . . . . . . . . . . . 16
3331, 32syl 16 . . . . . . . . . . . . . . 15
3430, 33sylan9eqr 2520 . . . . . . . . . . . . . 14
3529, 34eleqtrd 2547 . . . . . . . . . . . . 13
36 el1o 7168 . . . . . . . . . . . . 13
3735, 36sylib 196 . . . . . . . . . . . 12
3837oveq1d 6311 . . . . . . . . . . 11
399adantr 465 . . . . . . . . . . . 12
40 oa0r 7207 . . . . . . . . . . . 12
4139, 40syl 16 . . . . . . . . . . 11
4238, 41eqtrd 2498 . . . . . . . . . 10
4342ex 434 . . . . . . . . 9
4431adantr 465 . . . . . . . . . . . . . 14
45 simprl 756 . . . . . . . . . . . . . 14
46 oecl 7206 . . . . . . . . . . . . . 14
4744, 45, 46syl2anc 661 . . . . . . . . . . . . 13
48 limom 6715 . . . . . . . . . . . . . 14
4944, 48jctir 538 . . . . . . . . . . . . 13
50 simplll 759 . . . . . . . . . . . . . 14
51 simprr 757 . . . . . . . . . . . . . . . 16
5251oveq2d 6312 . . . . . . . . . . . . . . 15
53 oesuc 7196 . . . . . . . . . . . . . . . 16
5444, 45, 53syl2anc 661 . . . . . . . . . . . . . . 15
5552, 54eqtrd 2498 . . . . . . . . . . . . . 14
5650, 55eleqtrd 2547 . . . . . . . . . . . . 13
57 omordlim 7245 . . . . . . . . . . . . 13
5847, 49, 56, 57syl21anc 1227 . . . . . . . . . . . 12
5947adantr 465 . . . . . . . . . . . . . . . . 17
60 nnon 6706 . . . . . . . . . . . . . . . . . 18
6160ad2antrl 727 . . . . . . . . . . . . . . . . 17
62 omcl 7205 . . . . . . . . . . . . . . . . 17
6359, 61, 62syl2anc 661 . . . . . . . . . . . . . . . 16
64 eloni 4893 . . . . . . . . . . . . . . . 16
6563, 64syl 16 . . . . . . . . . . . . . . 15
66 simprr 757 . . . . . . . . . . . . . . 15
67 ordelss 4899 . . . . . . . . . . . . . . 15
6865, 66, 67syl2anc 661 . . . . . . . . . . . . . 14
6918ad2antrr 725 . . . . . . . . . . . . . . 15
709ad2antrr 725 . . . . . . . . . . . . . . 15
71 oawordri 7218 . . . . . . . . . . . . . . 15
7269, 63, 70, 71syl3anc 1228 . . . . . . . . . . . . . 14
7368, 72mpd 15 . . . . . . . . . . . . 13
7444adantr 465 . . . . . . . . . . . . . . . 16
75 odi 7247 . . . . . . . . . . . . . . . 16
7659, 61, 74, 75syl3anc 1228 . . . . . . . . . . . . . . 15
77 simprl 756 . . . . . . . . . . . . . . . . 17
78 oaabslem 7311 . . . . . . . . . . . . . . . . 17
7974, 77, 78syl2anc 661 . . . . . . . . . . . . . . . 16
8079oveq2d 6312 . . . . . . . . . . . . . . 15
8176, 80eqtr3d 2500 . . . . . . . . . . . . . 14
8255adantr 465 . . . . . . . . . . . . . . 15
8382oveq2d 6312 . . . . . . . . . . . . . 14
8481, 83, 823eqtr4d 2508 . . . . . . . . . . . . 13
8573, 84sseqtrd 3539 . . . . . . . . . . . 12
8658, 85rexlimddv 2953 . . . . . . . . . . 11
87 oaword2 7221 . . . . . . . . . . . . 13
889, 18, 87syl2anc 661 . . . . . . . . . . . 12
8988adantr 465 . . . . . . . . . . 11
9086, 89eqssd 3520 . . . . . . . . . 10
9190rexlimdvaa 2950 . . . . . . . . 9
92 simplll 759 . . . . . . . . . . . . . 14
9331adantr 465 . . . . . . . . . . . . . . 15
9424adantr 465 . . . . . . . . . . . . . . 15
95 simpr 461 . . . . . . . . . . . . . . 15
96 oelim2 7263 . . . . . . . . . . . . . . 15
9793, 94, 95, 96syl12anc 1226 . . . . . . . . . . . . . 14
9892, 97eleqtrd 2547 . . . . . . . . . . . . 13
99 eliun 4335 . . . . . . . . . . . . 13
10098, 99sylib 196 . . . . . . . . . . . 12
101 eldifi 3625 . . . . . . . . . . . . . 14
10218ad2antrr 725 . . . . . . . . . . . . . . . . 17
1039ad2antrr 725 . . . . . . . . . . . . . . . . 17
10493adantr 465 . . . . . . . . . . . . . . . . . . 19
105 1onn 7307 . . . . . . . . . . . . . . . . . . . 20
106105a1i 11 . . . . . . . . . . . . . . . . . . 19
107 ondif2 7171 . . . . . . . . . . . . . . . . . . 19
108104, 106, 107sylanbrc 664 . . . . . . . . . . . . . . . . . 18
10994adantr 465 . . . . . . . . . . . . . . . . . 18
110 simplr 755 . . . . . . . . . . . . . . . . . 18
111 oelimcl 7268 . . . . . . . . . . . . . . . . . 18
112108, 109, 110, 111syl12anc 1226 . . . . . . . . . . . . . . . . 17
113 oalim 7201 . . . . . . . . . . . . . . . . 17
114102, 103, 112, 113syl12anc 1226 . . . . . . . . . . . . . . . 16
115 oelim2 7263 . . . . . . . . . . . . . . . . . . . . . . 23
11693, 94, 95, 115syl12anc 1226 . . . . . . . . . . . . . . . . . . . . . 22
117116eleq2d 2527 . . . . . . . . . . . . . . . . . . . . 21
118 eliun 4335 . . . . . . . . . . . . . . . . . . . . 21
119117, 118syl6bb 261 . . . . . . . . . . . . . . . . . . . 20
120119adantr 465 . . . . . . . . . . . . . . . . . . 19
121 eldifi 3625 . . . . . . . . . . . . . . . . . . . . 21
122104adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
123109adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
124 simplrl 761 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
125 onelon 4908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126123, 124, 125syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
127122, 126, 46syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
128 eloni 4893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
129127, 128syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
130 simplrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131 ordelss 4899 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
132129, 130, 131syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
133 ssun1 3666 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
13426ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
135 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
136 ordunel 6662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
137134, 124, 135, 136syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30