oaabs2 - Metamath Proof Explorer

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

Theorem oaabs2 7725

Description: The absorption law oaabs 7724 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 3920	. . . . . . 7
2		fnoe 7590	. . . . . . . . 9
3		fndm 5990	. . . . . . . . 9
4	2, 3	ax-mp 5	. . . . . . . 8
5	4	ndmov 6818	. . . . . . 7 $/\$
6	1, 5	nsyl2 142	. . . . . 6 $/\$
7	6	ad2antrr 762	. . . . 5 $/\$ $/\$ $/\$
8		oecl 7617	. . . . 5 $/\$
9	7, 8	syl 17	. . . 4 $/\$ $/\$
10		simplr 792	. . . 4 $/\$ $/\$
11		simpr 477	. . . 4 $/\$ $/\$
12		oawordeu 7635	. . . 4 $/\$ $/\$
13	9, 10, 11, 12	syl21anc 1325	. . 3 $/\$ $/\$
14		reurex 3160	. . 3
15	13, 14	syl 17	. 2 $/\$ $/\$
16		simpll 790	. . . . . . . 8 $/\$ $/\$
17		onelon 5748	. . . . . . . 8 $/\$
18	9, 16, 17	syl2anc 693	. . . . . . 7 $/\$ $/\$
19	18	adantr 481	. . . . . 6 $/\$ $/\$ $/\$
20	9	adantr 481	. . . . . 6 $/\$ $/\$ $/\$
21		simpr 477	. . . . . 6 $/\$ $/\$ $/\$
22		oaass 7641	. . . . . 6 $/\$ $/\$
23	19, 20, 21, 22	syl3anc 1326	. . . . 5 $/\$ $/\$ $/\$
24	7	simprd 479	. . . . . . . . . 10 $/\$ $/\$
25		eloni 5733	. . . . . . . . . 10
26	24, 25	syl 17	. . . . . . . . 9 $/\$ $/\$
27		ordzsl 7045	. . . . . . . . 9 $\/$ $\/$
28	26, 27	sylib 208	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
29		simplll 798	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
30		oveq2 6658	. . . . . . . . . . . . . . 15
31	7	simpld 475	. . . . . . . . . . . . . . . 16 $/\$ $/\$
32		oe0 7602	. . . . . . . . . . . . . . . 16
33	31, 32	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$
34	30, 33	sylan9eqr 2678	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
35	29, 34	eleqtrd 2703	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
36		el1o 7579	. . . . . . . . . . . . 13
37	35, 36	sylib 208	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
38	37	oveq1d 6665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
39	9	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
40		oa0r 7618	. . . . . . . . . . . 12
41	39, 40	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$
42	38, 41	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$ $/\$
43	42	ex 450	. . . . . . . . 9 $/\$ $/\$
44	31	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
45		simprl 794	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
46		oecl 7617	. . . . . . . . . . . . . 14 $/\$
47	44, 45, 46	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
48		limom 7080	. . . . . . . . . . . . . 14
49	44, 48	jctir 561	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
50		simplll 798	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
51		simprr 796	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
52	51	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
53		oesuc 7607	. . . . . . . . . . . . . . . 16 $/\$
54	44, 45, 53	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
55	52, 54	eqtrd 2656	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
56	50, 55	eleqtrd 2703	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
57		omordlim 7657	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
58	47, 49, 56, 57	syl21anc 1325	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
59	47	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
60		nnon 7071	. . . . . . . . . . . . . . . . . 18
61	60	ad2antrl 764	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
62		omcl 7616	. . . . . . . . . . . . . . . . 17 $/\$
63	59, 61, 62	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
64		eloni 5733	. . . . . . . . . . . . . . . 16
65	63, 64	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66		simprr 796	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		ordelss 5739	. . . . . . . . . . . . . . 15 $/\$
68	65, 66, 67	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	18	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	9	ad2antrr 762	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71		oawordri 7630	. . . . . . . . . . . . . . 15 $/\$ $/\$
72	69, 63, 70, 71	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73	68, 72	mpd 15	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74	44	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
75		odi 7659	. . . . . . . . . . . . . . . 16 $/\$ $/\$
76	59, 61, 74, 75	syl3anc 1326	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
77		simprl 794	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78		oaabslem 7723	. . . . . . . . . . . . . . . . 17 $/\$
79	74, 77, 78	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
80	79	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
81	76, 80	eqtr3d 2658	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
82	55	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
83	82	oveq2d 6666	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
84	81, 83, 82	3eqtr4d 2666	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
85	73, 84	sseqtrd 3641	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
86	58, 85	rexlimddv 3035	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
87		oaword2 7633	. . . . . . . . . . . . 13 $/\$
88	9, 18, 87	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$
89	88	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
90	86, 89	eqssd 3620	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
91	90	rexlimdvaa 3032	. . . . . . . . 9 $/\$ $/\$
92		simplll 798	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
93	31	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
94	24	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
95		simpr 477	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
96		oelim2 7675	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$
97	93, 94, 95, 96	syl12anc 1324	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
98	92, 97	eleqtrd 2703	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
99		eliun 4524	. . . . . . . . . . . . 13 $\$ $\$
100	98, 99	sylib 208	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
101		eldifi 3732	. . . . . . . . . . . . . 14 $\$
102	18	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
103	9	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
104	93	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
105		1onn 7719	. . . . . . . . . . . . . . . . . . . 20
106	105	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
107		ondif2 7582	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$
108	104, 106, 107	sylanbrc 698	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
109	94	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
110		simplr 792	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
111		oelimcl 7680	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$
112	108, 109, 110, 111	syl12anc 1324	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
113		oalim 7612	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
114	102, 103, 112, 113	syl12anc 1324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
115		oelim2 7675	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $\$
116	93, 94, 95, 115	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $\$
117	116	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $\$
118		eliun 4524	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
119	117, 118	syl6bb 276	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\$
120	119	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
121		eldifi 3732	. . . . . . . . . . . . . . . . . . . . 21 $\$
122	104	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
123	109	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
124		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
125		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
126	123, 124, 125	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
127	122, 126, 46	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
128		eloni 5733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
129	127, 128	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130		simplrr 801	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
131		ordelss 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
132	129, 130, 131	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
133		ssun1 3776	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	26	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136		ordunel 7027	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
137	134, 124, 135, 136	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
138		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
139	123, 137, 138	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140		peano1 7085	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
141	140	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
142		oewordi 7671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
143	126, 139, 122, 141, 142	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
144	133, 143	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	132, 144	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	102	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147		oecl 7617	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
148	122, 139, 147	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
149		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
150	123, 135, 149	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
151		oecl 7617	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
152	122, 150, 151	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
155	152, 153, 154	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156		oawordri 7630	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
157	146, 148, 155, 156	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	145, 157	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
159		eloni 5733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
160	152, 159	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161		ordelss 5739	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162	160, 153, 161	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163		ssun2 3777	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
164		oewordi 7671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
165	150, 139, 122, 141, 164	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	163, 165	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	162, 166	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168		oaword 7629	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
169	155, 148, 148, 168	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
170	167, 169	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
171	158, 170	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
172		ordom 7074	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
173		ordsucss 7018	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
174	172, 105, 173	mp2 9	. . . . . . . . . . . . . . . . . . . . . . . . . 26
175		1on 7567	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
176		suceloni 7013	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
177	175, 176	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178		omwordi 7651	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
179	177, 122, 148, 178	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
180	174, 179	mpi 20	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182		omsuc 7606	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
183	148, 181, 182	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184		om1 7622	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
185	148, 184	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
186	185	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	183, 186	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188		oesuc 7607	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
189	122, 139, 188	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190	180, 187, 189	3sstr4d 3648	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
191	171, 190	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
192		ordsucss 7018	. . . . . . . . . . . . . . . . . . . . . . . . 25
193	134, 137, 192	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
194		suceloni 7013	. . . . . . . . . . . . . . . . . . . . . . . . . 26
195	139, 194	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
196		oewordi 7671	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
197	195, 123, 122, 141, 196	syl31anc 1329	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
198	193, 197	mpd 15	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
199	191, 198	sstrd 3613	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
200	199	expr 643	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
201	121, 200	sylan2 491	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\$
202	201	rexlimdva 3031	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $\$
203	120, 202	sylbid 230	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
204	203	ralrimiv 2965	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
205		iunss 4561	. . . . . . . . . . . . . . . . 17
206	204, 205	sylibr 224	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
207	114, 206	eqsstrd 3639	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
208	207	expr 643	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
209	101, 208	sylan2 491	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $\$
210	209	rexlimdva 3031	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
211	100, 210	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$
212	88	adantr 481	. . . . . . . . . . 11 $/\$ $/\$ $/\$
213	211, 212	eqssd 3620	. . . . . . . . . 10 $/\$ $/\$ $/\$
214	213	ex 450	. . . . . . . . 9 $/\$ $/\$
215	43, 91, 214	3jaod 1392	. . . . . . . 8 $/\$ $/\$ $\/$ $\/$
216	28, 215	mpd 15	. . . . . . 7 $/\$ $/\$
217	216	adantr 481	. . . . . 6 $/\$ $/\$ $/\$
218	217	oveq1d 6665	. . . . 5 $/\$ $/\$ $/\$
219	23, 218	eqtr3d 2658	. . . 4 $/\$ $/\$ $/\$
220		oveq2 6658	. . . . 5
221		id 22	. . . . 5
222	220, 221	eqeq12d 2637	. . . 4
223	219, 222	syl5ibcom 235	. . 3 $/\$ $/\$ $/\$
224	223	rexlimdva 3031	. 2 $/\$ $/\$
225	15, 224	mpd 15	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $/\$ wa 384 $\/$ w3o 1036

wceq 1483

wcel 1990

wral 2912

wrex 2913

wreu 2914 $\$ cdif 3571

cun 3572

wss 3574

c0 3915

ciun 4520

cxp 5112

cdm 5114

word 5722

con0 5723

wlim 5724

csuc 5725

wfn 5883 (class class class)co 6650

com 7065

c1o 7553

c2o 7554

coa 7557

comu 7558

coe 7559

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-oexp 7566

This theorem is referenced by: cnfcomlem 8596

W3C validator