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.

Step	Hyp	Ref	Expression
1		n0i 3789	. . . . . . 7
2		fnoe 7179	. . . . . . . . 9
3		fndm 5685	. . . . . . . . 9
4	2, 3	ax-mp 5	. . . . . . . 8
5	4	ndmov 6459	. . . . . . 7
6	1, 5	nsyl2 127	. . . . . 6
7	6	ad2antrr 725	. . . . 5
8		oecl 7206	. . . . 5
9	7, 8	syl 16	. . . 4
10		simplr 755	. . . 4
11		simpr 461	. . . 4
12		oawordeu 7223	. . . 4
13	9, 10, 11, 12	syl21anc 1227	. . 3
14		reurex 3074	. . 3
15	13, 14	syl 16	. 2
16		simpll 753	. . . . . . . 8
17		onelon 4908	. . . . . . . 8
18	9, 16, 17	syl2anc 661	. . . . . . 7
19	18	adantr 465	. . . . . 6
20	9	adantr 465	. . . . . 6
21		simpr 461	. . . . . 6
22		oaass 7229	. . . . . 6
23	19, 20, 21, 22	syl3anc 1228	. . . . 5
24	7	simprd 463	. . . . . . . . . 10
25		eloni 4893	. . . . . . . . . 10
26	24, 25	syl 16	. . . . . . . . 9
27		ordzsl 6680	. . . . . . . . 9
28	26, 27	sylib 196	. . . . . . . 8
29		simplll 759	. . . . . . . . . . . . . 14
30		oveq2 6304	. . . . . . . . . . . . . . 15
31	7	simpld 459	. . . . . . . . . . . . . . . 16
32		oe0 7191	. . . . . . . . . . . . . . . 16
33	31, 32	syl 16	. . . . . . . . . . . . . . 15
34	30, 33	sylan9eqr 2520	. . . . . . . . . . . . . 14
35	29, 34	eleqtrd 2547	. . . . . . . . . . . . 13
36		el1o 7168	. . . . . . . . . . . . 13
37	35, 36	sylib 196	. . . . . . . . . . . 12
38	37	oveq1d 6311	. . . . . . . . . . 11
39	9	adantr 465	. . . . . . . . . . . 12
40		oa0r 7207	. . . . . . . . . . . 12
41	39, 40	syl 16	. . . . . . . . . . 11
42	38, 41	eqtrd 2498	. . . . . . . . . 10
43	42	ex 434	. . . . . . . . 9
44	31	adantr 465	. . . . . . . . . . . . . 14
45		simprl 756	. . . . . . . . . . . . . 14
46		oecl 7206	. . . . . . . . . . . . . 14
47	44, 45, 46	syl2anc 661	. . . . . . . . . . . . 13
48		limom 6715	. . . . . . . . . . . . . 14
49	44, 48	jctir 538	. . . . . . . . . . . . 13
50		simplll 759	. . . . . . . . . . . . . 14
51		simprr 757	. . . . . . . . . . . . . . . 16
52	51	oveq2d 6312	. . . . . . . . . . . . . . 15
53		oesuc 7196	. . . . . . . . . . . . . . . 16
54	44, 45, 53	syl2anc 661	. . . . . . . . . . . . . . 15
55	52, 54	eqtrd 2498	. . . . . . . . . . . . . 14
56	50, 55	eleqtrd 2547	. . . . . . . . . . . . 13
57		omordlim 7245	. . . . . . . . . . . . 13
58	47, 49, 56, 57	syl21anc 1227	. . . . . . . . . . . 12
59	47	adantr 465	. . . . . . . . . . . . . . . . 17
60		nnon 6706	. . . . . . . . . . . . . . . . . 18
61	60	ad2antrl 727	. . . . . . . . . . . . . . . . 17
62		omcl 7205	. . . . . . . . . . . . . . . . 17
63	59, 61, 62	syl2anc 661	. . . . . . . . . . . . . . . 16
64		eloni 4893	. . . . . . . . . . . . . . . 16
65	63, 64	syl 16	. . . . . . . . . . . . . . 15
66		simprr 757	. . . . . . . . . . . . . . 15
67		ordelss 4899	. . . . . . . . . . . . . . 15
68	65, 66, 67	syl2anc 661	. . . . . . . . . . . . . 14
69	18	ad2antrr 725	. . . . . . . . . . . . . . 15
70	9	ad2antrr 725	. . . . . . . . . . . . . . 15
71		oawordri 7218	. . . . . . . . . . . . . . 15
72	69, 63, 70, 71	syl3anc 1228	. . . . . . . . . . . . . 14
73	68, 72	mpd 15	. . . . . . . . . . . . 13
74	44	adantr 465	. . . . . . . . . . . . . . . 16
75		odi 7247	. . . . . . . . . . . . . . . 16
76	59, 61, 74, 75	syl3anc 1228	. . . . . . . . . . . . . . 15
77		simprl 756	. . . . . . . . . . . . . . . . 17
78		oaabslem 7311	. . . . . . . . . . . . . . . . 17
79	74, 77, 78	syl2anc 661	. . . . . . . . . . . . . . . 16
80	79	oveq2d 6312	. . . . . . . . . . . . . . 15
81	76, 80	eqtr3d 2500	. . . . . . . . . . . . . 14
82	55	adantr 465	. . . . . . . . . . . . . . 15
83	82	oveq2d 6312	. . . . . . . . . . . . . 14
84	81, 83, 82	3eqtr4d 2508	. . . . . . . . . . . . 13
85	73, 84	sseqtrd 3539	. . . . . . . . . . . 12
86	58, 85	rexlimddv 2953	. . . . . . . . . . 11
87		oaword2 7221	. . . . . . . . . . . . 13
88	9, 18, 87	syl2anc 661	. . . . . . . . . . . 12
89	88	adantr 465	. . . . . . . . . . 11
90	86, 89	eqssd 3520	. . . . . . . . . 10
91	90	rexlimdvaa 2950	. . . . . . . . 9
92		simplll 759	. . . . . . . . . . . . . 14
93	31	adantr 465	. . . . . . . . . . . . . . 15
94	24	adantr 465	. . . . . . . . . . . . . . 15
95		simpr 461	. . . . . . . . . . . . . . 15
96		oelim2 7263	. . . . . . . . . . . . . . 15
97	93, 94, 95, 96	syl12anc 1226	. . . . . . . . . . . . . 14
98	92, 97	eleqtrd 2547	. . . . . . . . . . . . 13
99		eliun 4335	. . . . . . . . . . . . 13
100	98, 99	sylib 196	. . . . . . . . . . . 12
101		eldifi 3625	. . . . . . . . . . . . . 14
102	18	ad2antrr 725	. . . . . . . . . . . . . . . . 17
103	9	ad2antrr 725	. . . . . . . . . . . . . . . . 17
104	93	adantr 465	. . . . . . . . . . . . . . . . . . 19
105		1onn 7307	. . . . . . . . . . . . . . . . . . . 20
106	105	a1i 11	. . . . . . . . . . . . . . . . . . 19
107		ondif2 7171	. . . . . . . . . . . . . . . . . . 19
108	104, 106, 107	sylanbrc 664	. . . . . . . . . . . . . . . . . 18
109	94	adantr 465	. . . . . . . . . . . . . . . . . 18
110		simplr 755	. . . . . . . . . . . . . . . . . 18
111		oelimcl 7268	. . . . . . . . . . . . . . . . . 18
112	108, 109, 110, 111	syl12anc 1226	. . . . . . . . . . . . . . . . 17
113		oalim 7201	. . . . . . . . . . . . . . . . 17
114	102, 103, 112, 113	syl12anc 1226	. . . . . . . . . . . . . . . 16
115		oelim2 7263	. . . . . . . . . . . . . . . . . . . . . . 23
116	93, 94, 95, 115	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . 22
117	116	eleq2d 2527	. . . . . . . . . . . . . . . . . . . . 21
118		eliun 4335	. . . . . . . . . . . . . . . . . . . . 21
119	117, 118	syl6bb 261	. . . . . . . . . . . . . . . . . . . 20
120	119	adantr 465	. . . . . . . . . . . . . . . . . . 19
121		eldifi 3625	. . . . . . . . . . . . . . . . . . . . 21
122	104	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
123	109	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
124		simplrl 761	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
125		onelon 4908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126	123, 124, 125	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
127	122, 126, 46	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
128		eloni 4893	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
129	127, 128	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
130		simplrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
131		ordelss 4899	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
132	129, 130, 131	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
133		ssun1 3666	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	26	ad3antrrr 729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
135		simprl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
136		ordunel 6662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
137	134, 124, 135, 136	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30