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

Theorem omabs 7315
Description: Ordinal multiplication is also absorbed by powers of . (Contributed by Mario Carneiro, 30-May-2015.)
Assertion
Ref Expression
omabs

Proof of Theorem omabs
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2530 . . . . . . . 8
2 oveq2 6304 . . . . . . . . . 10
32oveq2d 6312 . . . . . . . . 9
43, 2eqeq12d 2479 . . . . . . . 8
51, 4imbi12d 320 . . . . . . 7
6 eleq2 2530 . . . . . . . 8
7 oveq2 6304 . . . . . . . . . 10
87oveq2d 6312 . . . . . . . . 9
98, 7eqeq12d 2479 . . . . . . . 8
106, 9imbi12d 320 . . . . . . 7
11 eleq2 2530 . . . . . . . 8
12 oveq2 6304 . . . . . . . . . 10
1312oveq2d 6312 . . . . . . . . 9
1413, 12eqeq12d 2479 . . . . . . . 8
1511, 14imbi12d 320 . . . . . . 7
16 eleq2 2530 . . . . . . . 8
17 oveq2 6304 . . . . . . . . . 10
1817oveq2d 6312 . . . . . . . . 9
1918, 17eqeq12d 2479 . . . . . . . 8
2016, 19imbi12d 320 . . . . . . 7
21 noel 3788 . . . . . . . . 9
2221pm2.21i 131 . . . . . . . 8
2322a1i 11 . . . . . . 7
24 simprl 756 . . . . . . . . . . . . . . . 16
25 simpll 753 . . . . . . . . . . . . . . . 16
26 simplr 755 . . . . . . . . . . . . . . . 16
27 omabslem 7314 . . . . . . . . . . . . . . . 16
2824, 25, 26, 27syl3anc 1228 . . . . . . . . . . . . . . 15
2928adantr 465 . . . . . . . . . . . . . 14
30 suceq 4948 . . . . . . . . . . . . . . . . . 18
31 df-1o 7149 . . . . . . . . . . . . . . . . . 18
3230, 31syl6eqr 2516 . . . . . . . . . . . . . . . . 17
3332oveq2d 6312 . . . . . . . . . . . . . . . 16
34 oe1 7212 . . . . . . . . . . . . . . . . 17
3534ad2antrl 727 . . . . . . . . . . . . . . . 16
3633, 35sylan9eqr 2520 . . . . . . . . . . . . . . 15
3736oveq2d 6312 . . . . . . . . . . . . . 14
3829, 37, 363eqtr4d 2508 . . . . . . . . . . . . 13
3938ex 434 . . . . . . . . . . . 12
4039a1dd 46 . . . . . . . . . . 11
41 oveq1 6303 . . . . . . . . . . . . . 14
42 oesuc 7196 . . . . . . . . . . . . . . . . . 18
4342adantl 466 . . . . . . . . . . . . . . . . 17
4443oveq2d 6312 . . . . . . . . . . . . . . . 16
45 nnon 6706 . . . . . . . . . . . . . . . . . 18
4645ad2antrr 725 . . . . . . . . . . . . . . . . 17
47 oecl 7206 . . . . . . . . . . . . . . . . . 18
4847adantl 466 . . . . . . . . . . . . . . . . 17
49 omass 7248 . . . . . . . . . . . . . . . . 17
5046, 48, 24, 49syl3anc 1228 . . . . . . . . . . . . . . . 16
5144, 50eqtr4d 2501 . . . . . . . . . . . . . . 15
5251, 43eqeq12d 2479 . . . . . . . . . . . . . 14
5341, 52syl5ibr 221 . . . . . . . . . . . . 13
5453imim2d 52 . . . . . . . . . . . 12
5554com23 78 . . . . . . . . . . 11
56 simprr 757 . . . . . . . . . . . 12
57 on0eqel 5000 . . . . . . . . . . . 12
5856, 57syl 16 . . . . . . . . . . 11
5940, 55, 58mpjaod 381 . . . . . . . . . 10
6059a1dd 46 . . . . . . . . 9
6160anassrs 648 . . . . . . . 8
6261expcom 435 . . . . . . 7
6345ad3antrrr 729 . . . . . . . . . . . . . 14
64 simprl 756 . . . . . . . . . . . . . . . 16
65 simprr 757 . . . . . . . . . . . . . . . . . 18
66 vex 3112 . . . . . . . . . . . . . . . . . 18
6765, 66jctil 537 . . . . . . . . . . . . . . . . 17
68 limelon 4946 . . . . . . . . . . . . . . . . 17
6967, 68syl 16 . . . . . . . . . . . . . . . 16
70 oecl 7206 . . . . . . . . . . . . . . . 16
7164, 69, 70syl2anc 661 . . . . . . . . . . . . . . 15
7271adantr 465 . . . . . . . . . . . . . 14
73 1onn 7307 . . . . . . . . . . . . . . . . . 18
7473a1i 11 . . . . . . . . . . . . . . . . 17
75 ondif2 7171 . . . . . . . . . . . . . . . . 17
7664, 74, 75sylanbrc 664 . . . . . . . . . . . . . . . 16
7776adantr 465 . . . . . . . . . . . . . . 15
7867adantr 465 . . . . . . . . . . . . . . 15
79 oelimcl 7268 . . . . . . . . . . . . . . 15
8077, 78, 79syl2anc 661 . . . . . . . . . . . . . 14
81 omlim 7202 . . . . . . . . . . . . . 14
8263, 72, 80, 81syl12anc 1226 . . . . . . . . . . . . 13
83 simplrl 761 . . . . . . . . . . . . . . . . . . . 20
84 oelim2 7263 . . . . . . . . . . . . . . . . . . . 20
8583, 78, 84syl2anc 661 . . . . . . . . . . . . . . . . . . 19
8685eleq2d 2527 . . . . . . . . . . . . . . . . . 18
87 eliun 4335 . . . . . . . . . . . . . . . . . 18
8886, 87syl6bb 261 . . . . . . . . . . . . . . . . 17
8969adantr 465 . . . . . . . . . . . . . . . . . 18
90 anass 649 . . . . . . . . . . . . . . . . . . . 20
91 onelon 4908 . . . . . . . . . . . . . . . . . . . . . . . 24
92 on0eln0 4938 . . . . . . . . . . . . . . . . . . . . . . . 24
9391, 92syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
9493pm5.32da 641 . . . . . . . . . . . . . . . . . . . . . 22
95 dif1o 7169 . . . . . . . . . . . . . . . . . . . . . 22
9694, 95syl6bbr 263 . . . . . . . . . . . . . . . . . . . . 21
9796anbi1d 704 . . . . . . . . . . . . . . . . . . . 20
9890, 97syl5bbr 259 . . . . . . . . . . . . . . . . . . 19
9998rexbidv2 2964 . . . . . . . . . . . . . . . . . 18
10089, 99syl 16 . . . . . . . . . . . . . . . . 17
10188, 100bitr4d 256 . . . . . . . . . . . . . . . 16
102 r19.29 2992 . . . . . . . . . . . . . . . . . 18
103 id 22 . . . . . . . . . . . . . . . . . . . . . . 23
104103imp 429 . . . . . . . . . . . . . . . . . . . . . 22
105104anim1i 568 . . . . . . . . . . . . . . . . . . . . 21
106105anasss 647 . . . . . . . . . . . . . . . . . . . 20
10771ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23
108 eloni 4893 . . . . . . . . . . . . . . . . . . . . . . 23
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . . . 22
110 simprr 757 . . . . . . . . . . . . . . . . . . . . . . . . 25
11164ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
11269ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
113 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
114112, 113, 91syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
115111, 114, 47syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
116 onelon 4908 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
117115, 110, 116syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11845ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
119118ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
120 simplr 755 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
121120ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
122 omord2 7235 . . . . . . . . . . . . . . . . . . . . . . . . . 26
123117, 115, 119, 121, 122syl31anc 1231 . . . . . . . . . . . . . . . . . . . . . . . . 25
124110, 123mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . 24
125 simprl 756 . . . . . . . . . . . . . . . . . . . . . . . 24
126124, 125eleqtrd 2547 . . . . . . . . . . . . . . . . . . . . . . 23
12776ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
128 oeord 7256 . . . . . . . . . . . . . . . . . . . . . . . . 25
129114, 112, 127, 128syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . 24
130113, 129mpbid 210 . . . . . . . . . . . . . . . . . . . . . . 23
131 ontr1 4929 . . . . . . . . . . . . . . . . . . . . . . . 24
132107, 131syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
133126, 130, 132mp2and 679 . . . . . . . . . . . . . . . . . . . . . 22
134 ordelss 4899 . . . . . . . . . . . . . . . . . . . . . 22
135109, 133, 134syl2anc 661 . . . . . . . . . . . . . . . . . . . . 21
136135ex 434 . . . . . . . . . . . . . . . . . . . 20
137106, 136syl5 32 . . . . . . . . . . . . . . . . . . 19
138137rexlimdva 2949 . . . . . . . . . . . . . . . . . 18