axcontlem2 - Metamath Proof Explorer

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

Theorem axcontlem2 25845

Description: Lemma for axcont 25856. The idea here is to set up a mapping

that will allow us to transfer dedekind 10200 to two sets of points. Here, we set up

and show its domain and range. (Contributed by Scott Fenton, 17-Jun-2013.)

**Hypotheses**
Ref	Expression
axcontlem2.1	$\/$
axcontlem2.2	$/\$ $/\$

**Assertion**
Ref	Expression
axcontlem2	$/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

Proof of Theorem axcontlem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq2 4403	. . . . . . . . . 10
2	1	breq2d 4665	. . . . . . . . 9
3		breq1 4656	. . . . . . . . 9
4	2, 3	orbi12d 746	. . . . . . . 8 $\/$ $\/$
5		axcontlem2.1	. . . . . . . 8 $\/$
6	4, 5	elrab2 3366	. . . . . . 7 $/\$ $\/$
7		simpll3 1102	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
8		simpll2 1101	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
9		simpr 477	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
10		brbtwn 25779	. . . . . . . . . . . 12 $/\$ $/\$
11	7, 8, 9, 10	syl3anc 1326	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
12	11	biimpa 501	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
13		simp-4r 807	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
14		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . 22
15		1m0e1 11131	. . . . . . . . . . . . . . . . . . . . . 22
16	14, 15	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21
17	16	oveq1d 6665	. . . . . . . . . . . . . . . . . . . 20
18		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20
19	17, 18	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
20	19	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18
21	20	ralbidv 2986	. . . . . . . . . . . . . . . . 17
22	21	biimpac 503	. . . . . . . . . . . . . . . 16 $/\$
23		eqcom 2629	. . . . . . . . . . . . . . . . 17
24	7	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
25	8	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
26		eqeefv 25783	. . . . . . . . . . . . . . . . . . 19 $/\$
27	24, 25, 26	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
28	8	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
29		fveecn 25782	. . . . . . . . . . . . . . . . . . . . 21 $/\$
30	28, 29	sylancom 701	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
31		simpllr 799	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
32		fveecn 25782	. . . . . . . . . . . . . . . . . . . . 21 $/\$
33	31, 32	sylancom 701	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
34		mulid2 10038	. . . . . . . . . . . . . . . . . . . . . . 23
35		mul02 10214	. . . . . . . . . . . . . . . . . . . . . . 23
36	34, 35	oveqan12d 6669	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
37		addid1 10216	. . . . . . . . . . . . . . . . . . . . . . 23
38	37	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
39	36, 38	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
40	39	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . 20 $/\$
41	30, 33, 40	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
42	41	ralbidva 2985	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
43	27, 42	bitr4d 271	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
44	23, 43	syl5bb 272	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
45	22, 44	syl5ibr 236	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
46	45	expdimp 453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
47	46	necon3d 2815	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
48	13, 47	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
49		0re 10040	. . . . . . . . . . . . . . . . . . . 20
50		1re 10039	. . . . . . . . . . . . . . . . . . . 20
51	49, 50	elicc2i 12239	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
52	51	simp1bi 1076	. . . . . . . . . . . . . . . . . 18
53		rereccl 10743	. . . . . . . . . . . . . . . . . 18 $/\$
54	52, 53	sylan 488	. . . . . . . . . . . . . . . . 17 $/\$
55	52	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
56	51	simp2bi 1077	. . . . . . . . . . . . . . . . . . . 20
57	56	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$
58		simpr 477	. . . . . . . . . . . . . . . . . . 19 $/\$
59	55, 57, 58	ne0gt0d 10174	. . . . . . . . . . . . . . . . . 18 $/\$
60		0le1 10551	. . . . . . . . . . . . . . . . . . 19
61		divge0 10892	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
62	50, 60, 61	mpanl12 718	. . . . . . . . . . . . . . . . . 18 $/\$
63	55, 59, 62	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$
64		elrege0 12278	. . . . . . . . . . . . . . . . 17 $/\$
65	54, 63, 64	sylanbrc 698	. . . . . . . . . . . . . . . 16 $/\$
66	65	adantll 750	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	52	ad3antlr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	67	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69		simplr 792	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70		simp-4r 807	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
71	70, 32	sylancom 701	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
72	8	ad3antrrr 766	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
73	72, 29	sylancom 701	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
74		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . . . 24
75		reccl 10692	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
76		subcl 10280	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
77	74, 75, 76	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
78	77	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
79		subcl 10280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
80	74, 79	mpan 706	. . . . . . . . . . . . . . . . . . . . . . . . 25
81	80	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
82	75, 81	mulcld 10060	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
83	82	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
84		simprr 796	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
85	78, 83, 84	adddird 10065	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
86		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
87		subdi 10463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
88	74, 87	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
89	75, 86, 88	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
90	89	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
91	75	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
92		recid2 10700	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
93	91, 92	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
94	93	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
95		addsubass 10291	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
96	74, 95	mp3an3 1413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
97	77, 75, 96	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
98	77, 75	addcld 10059	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
99		npcan 10290	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
100	74, 75, 99	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
101	98, 100	subeq0bd 10456	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
102	94, 97, 101	3eqtr2d 2662	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
103	90, 102	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
104	103	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
105	104	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
106	75	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
107	80	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
108	106, 107, 84	mulassd 10063	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
109	108	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
110	85, 105, 109	3eqtr3rd 2665	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
111		mul02 10214	. . . . . . . . . . . . . . . . . . . . 21
112	111	ad2antll 765	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
113	110, 112	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
114		simpll 790	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
115		simprl 794	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
116	106, 114, 115	mulassd 10063	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
117	92	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 $/\$
118		mulid2 10038	. . . . . . . . . . . . . . . . . . . . . 22
119	118	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
120	117, 119	sylan9eq 2676	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
121	116, 120	eqtr3d 2658	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
122	113, 121	oveq12d 6668	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
123	78, 84	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
124		simpr 477	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
125		mulcl 10020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
126	81, 124, 125	syl2an 494	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
127	106, 126	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
128		mulcl 10020	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
129	128	ad2ant2r 783	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
130	106, 129	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
131	123, 127, 130	addassd 10062	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
132	106, 126, 129	adddid 10064	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
133	132	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
134	131, 133	eqtr4d 2659	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
135		addid2 10219	. . . . . . . . . . . . . . . . . . 19
136	135	ad2antrl 764	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
137	122, 134, 136	3eqtr3rd 2665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
138	68, 69, 71, 73, 137	syl22anc 1327	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
139	138	ralrimiva 2966	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
140		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20
141	140	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19
142		oveq1 6657	. . . . . . . . . . . . . . . . . . 19
143	141, 142	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
144	143	eqeq2d 2632	. . . . . . . . . . . . . . . . 17
145	144	ralbidv 2986	. . . . . . . . . . . . . . . 16
146	145	rspcev 3309	. . . . . . . . . . . . . . 15 $/\$
147	66, 139, 146	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
148		oveq2 6658	. . . . . . . . . . . . . . . . . . 19
149	148	oveq2d 6666	. . . . . . . . . . . . . . . . . 18
150	149	eqeq2d 2632	. . . . . . . . . . . . . . . . 17
151	150	ralimi 2952	. . . . . . . . . . . . . . . 16
152		ralbi 3068	. . . . . . . . . . . . . . . 16
153	151, 152	syl 17	. . . . . . . . . . . . . . 15
154	153	rexbidv 3052	. . . . . . . . . . . . . 14
155	147, 154	syl5ibrcom 237	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156	155	impancom 456	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
157	48, 156	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	157	r19.29an 3077	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
159	12, 158	syldan 487	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
160		3simpa 1058	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
161	49, 50	elicc2i 12239	. . . . . . . . . . . 12 $/\$ $/\$
162		elrege0 12278	. . . . . . . . . . . 12 $/\$
163	160, 161, 162	3imtr4i 281	. . . . . . . . . . 11
164	163	ssriv 3607	. . . . . . . . . 10
165		brbtwn 25779	. . . . . . . . . . . 12 $/\$ $/\$
166	9, 8, 7, 165	syl3anc 1326	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
167	166	biimpa 501	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
168		ssrexv 3667	. . . . . . . . . 10
169	164, 167, 168	mpsyl 68	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
170	159, 169	jaodan 826	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
171	170	anasss 679	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
172	6, 171	sylan2b 492	. . . . . 6 $/\$ $/\$ $/\$ $/\$
173		r19.26 3064	. . . . . . . . . 10 $/\$ $/\$
174		eqtr2 2642	. . . . . . . . . . 11 $/\$
175	174	ralimi 2952	. . . . . . . . . 10 $/\$
176	173, 175	sylbir 225	. . . . . . . . 9 $/\$
177		elrege0 12278	. . . . . . . . . . . . 13 $/\$
178	177	simplbi 476	. . . . . . . . . . . 12
179	178	recnd 10068	. . . . . . . . . . 11
180		elrege0 12278	. . . . . . . . . . . . 13 $/\$
181	180	simplbi 476	. . . . . . . . . . . 12
182	181	recnd 10068	. . . . . . . . . . 11
183	179, 182	anim12i 590	. . . . . . . . . 10 $/\$ $/\$
184		simplr 792	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
185		simpl2 1065	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
186	185	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
187	186, 29	sylancom 701	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
188		simpl3 1066	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
189	188	ad2antrr 762	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
190		fveecn 25782	. . . . . . . . . . . . . 14 $/\$
191	189, 190	sylancom 701	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
192		subcl 10280	. . . . . . . . . . . . . . . . . 18 $/\$
193	74, 192	mpan 706	. . . . . . . . . . . . . . . . 17
194	193	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
195		simpl 473	. . . . . . . . . . . . . . . 16 $/\$
196		mulcl 10020	. . . . . . . . . . . . . . . 16 $/\$
197	194, 195, 196	syl2an 494	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
198		mulcl 10020	. . . . . . . . . . . . . . . 16 $/\$
199	198	ad2ant2rl 785	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
200	80	adantl 482	. . . . . . . . . . . . . . . 16 $/\$
201	200, 195, 125	syl2an 494	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
202		mulcl 10020	. . . . . . . . . . . . . . . 16 $/\$
203	202	ad2ant2l 782	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
204	197, 199, 201, 203	addsubeq4d 10443	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
205		nnncan1 10317	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
206	74, 205	mp3an1 1411	. . . . . . . . . . . . . . . . . . 19 $/\$
207	206	ancoms 469	. . . . . . . . . . . . . . . . . 18 $/\$
208	207	oveq1d 6665	. . . . . . . . . . . . . . . . 17 $/\$
209	208	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
210	80	ad2antlr 763	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
211	193	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
212		simprl 794	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
213	210, 211, 212	subdird 10487	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
214	209, 213	eqtr3d 2658	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
215		simpll 790	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
216		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
217		simprr 796	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
218	215, 216, 217	subdird 10487	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
219	214, 218	eqeq12d 2637	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
220		subcl 10280	. . . . . . . . . . . . . . . 16 $/\$
221	220	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
222		mulcan1g 10680	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
223	221, 212, 217, 222	syl3anc 1326	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\/$
224	204, 219, 223	3bitr2d 296	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$
225	184, 187, 191, 224	syl12anc 1324	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
226	225	ralbidva 2985	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
227		r19.32v 3083	. . . . . . . . . . . 12 $\/$ $\/$
228		simplr 792	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
229	228	neneqd 2799	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
230		simpll2 1101	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
231		simpll3 1102	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
232		eqeefv 25783	. . . . . . . . . . . . . . . 16 $/\$
233	230, 231, 232	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
234	229, 233	mtbid 314	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
235		orel2 398	. . . . . . . . . . . . . 14 $\/$
236	234, 235	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
237		subeq0 10307	. . . . . . . . . . . . . 14 $/\$
238	237	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
239	236, 238	sylibd 229	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
240	227, 239	syl5bi 232	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
241	226, 240	sylbid 230	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
242	183, 241	sylan2 491	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
243	176, 242	syl5 34	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
244	243	ralrimivva 2971	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
245	244	adantr 481	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
246		oveq2 6658	. . . . . . . . . . 11
247	246	oveq1d 6665	. . . . . . . . . 10
248		oveq1 6657	. . . . . . . . . 10
249	247, 248	oveq12d 6668	. . . . . . . . 9
250	249	eqeq2d 2632	. . . . . . . 8
251	250	ralbidv 2986	. . . . . . 7
252	251	reu4 3400	. . . . . 6 $/\$ $/\$
253	172, 245, 252	sylanbrc 698	. . . . 5 $/\$ $/\$ $/\$ $/\$
254		df-reu 2919	. . . . 5 $/\$
255	253, 254	sylib 208	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
256	255	ralrimiva 2966	. . 3 $/\$ $/\$ $/\$ $/\$
257		axcontlem2.2	. . . 4 $/\$ $/\$
258	257	fnopabg 6017	. . 3 $/\$
259	256, 258	sylib 208	. 2 $/\$ $/\$ $/\$
260	178	ad2antlr 763	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
261	185	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
262		fveere 25781	. . . . . . . . . . 11 $/\$
263	261, 262	sylancom 701	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
264	188	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
265		fveere 25781	. . . . . . . . . . 11 $/\$
266	264, 265	sylancom 701	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
267		resubcl 10345	. . . . . . . . . . . . . 14 $/\$
268	50, 267	mpan 706	. . . . . . . . . . . . 13
269		remulcl 10021	. . . . . . . . . . . . 13 $/\$
270	268, 269	sylan 488	. . . . . . . . . . . 12 $/\$
271	270	3adant3 1081	. . . . . . . . . . 11 $/\$ $/\$
272		remulcl 10021	. . . . . . . . . . . 12 $/\$
273	272	3adant2 1080	. . . . . . . . . . 11 $/\$ $/\$
274	271, 273	readdcld 10069	. . . . . . . . . 10 $/\$ $/\$
275	260, 263, 266, 274	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
276	275	ralrimiva 2966	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
277		simpll1 1100	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
278		mptelee 25775	. . . . . . . . 9
279	277, 278	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
280	276, 279	mpbird 247	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
281		letric 10137	. . . . . . . . . 10 $/\$ $\/$
282	50, 178, 281	sylancr 695	. . . . . . . . 9 $\/$
283	282	adantl 482	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$
284		simpr 477	. . . . . . . . . . . . . 14 $/\$
285	178	adantr 481	. . . . . . . . . . . . . . 15 $/\$
286		0red 10041	. . . . . . . . . . . . . . . 16 $/\$
287		1red 10055	. . . . . . . . . . . . . . . 16 $/\$
288		0lt1 10550	. . . . . . . . . . . . . . . . 17
289	288	a1i 11	. . . . . . . . . . . . . . . 16 $/\$
290	286, 287, 285, 289, 284	ltletrd 10197	. . . . . . . . . . . . . . 15 $/\$
291		divelunit 12314	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
292	50, 60, 291	mpanl12 718	. . . . . . . . . . . . . . 15 $/\$
293	285, 290, 292	syl2anc 693	. . . . . . . . . . . . . 14 $/\$
294	284, 293	mpbird 247	. . . . . . . . . . . . 13 $/\$
295	294	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
296	178	ad3antlr 767	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
297	296	recnd 10068	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
298	290	gt0ne0d 10592	. . . . . . . . . . . . . . . 16 $/\$
299	298	adantll 750	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
300	299	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
301	185	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
302	301, 29	sylancom 701	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
303	188	ad3antrrr 766	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
304	303, 190	sylancom 701	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
305		reccl 10692	. . . . . . . . . . . . . . . . . 18 $/\$
306	305	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
307	193	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$
308	307, 195, 196	syl2an 494	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
309	198	ad2ant2rl 785	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
310	306, 308, 309	adddid 10064	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
311	310	oveq2d 6666	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
312		subcl 10280	. . . . . . . . . . . . . . . . . 18 $/\$
313	74, 305, 312	sylancr 695	. . . . . . . . . . . . . . . . 17 $/\$
314		mulcl 10020	. . . . . . . . . . . . . . . . 17 $/\$
315	313, 195, 314	syl2an 494	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
316	306, 308	mulcld 10060	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
317		recid2 10700	. . . . . . . . . . . . . . . . . . . 20 $/\$
318	317	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 $/\$
319	318	adantr 481	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
320		simpll 790	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
321		simprr 796	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
322	306, 320, 321	mulassd 10063	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
323		mulid2 10038	. . . . . . . . . . . . . . . . . . 19
324	323	ad2antll 765	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
325	319, 322, 324	3eqtr3d 2664	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
326	325, 321	eqeltrd 2701	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
327	315, 316, 326	addassd 10062	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
328	313	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
329	305, 307	mulcld 10060	. . . . . . . . . . . . . . . . . . . 20 $/\$
330	329	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
331		simprl 794	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
332	328, 330, 331	adddird 10065	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
333		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
334		subdi 10463	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
335	74, 334	mp3an2 1412	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
336	305, 333, 335	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
337	305	mulid1d 10057	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
338	337, 317	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
339	336, 338	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
340	339	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
341		npncan2 10308	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
342	74, 305, 341	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
343	340, 342	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
344	343	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
345	344	oveq1d 6665	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
346	111	ad2antrl 764	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
347	345, 346	eqtrd 2656	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
348	193	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
349	306, 348, 331	mulassd 10063	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
350	349	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
351	332, 347, 350	3eqtr3rd 2665	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
352	351, 325	oveq12d 6668	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
353		addid2 10219	. . . . . . . . . . . . . . . . 17
354	353	ad2antll 765	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
355	352, 354	eqtrd 2656	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
356	311, 327, 355	3eqtr2rd 2663	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
357	297, 300, 302, 304, 356	syl22anc 1327	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
358	357	ralrimiva 2966	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
359		oveq2 6658	. . . . . . . . . . . . . . . . . 18
360	359	oveq1d 6665	. . . . . . . . . . . . . . . . 17
361		oveq1 6657	. . . . . . . . . . . . . . . . 17
362	360, 361	oveq12d 6668	. . . . . . . . . . . . . . . 16
363	362	eqeq2d 2632	. . . . . . . . . . . . . . 15
364	363	ralbidv 2986	. . . . . . . . . . . . . 14
365		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
366	365	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
367		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
368	367	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20
369	366, 368	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19
370		eqid 2622	. . . . . . . . . . . . . . . . . . 19
371		ovex 6678	. . . . . . . . . . . . . . . . . . 19
372	369, 370, 371	fvmpt 6282	. . . . . . . . . . . . . . . . . 18
373	372	oveq2d 6666	. . . . . . . . . . . . . . . . 17
374	373	oveq2d 6666	. . . . . . . . . . . . . . . 16
375	374	eqeq2d 2632	. . . . . . . . . . . . . . 15
376	375	ralbiia 2979	. . . . . . . . . . . . . 14
377	364, 376	syl6bb 276	. . . . . . . . . . . . 13
378	377	rspcev 3309	. . . . . . . . . . . 12 $/\$
379	295, 358, 378	syl2anc 693	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
380	188	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
381	185	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
382	280	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
383		brbtwn 25779	. . . . . . . . . . . 12 $/\$ $/\$
384	380, 381, 382, 383	syl3anc 1326	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
385	379, 384	mpbird 247	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
386	385	ex 450	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
387		simpll 790	. . . . . . . . . . . . . . 15 $/\$ $/\$
388		simplr 792	. . . . . . . . . . . . . . 15 $/\$ $/\$
389		simpr 477	. . . . . . . . . . . . . . 15 $/\$ $/\$
390	387, 388, 389	3jca 1242	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
391	177	anbi1i 731	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
392	49, 50	elicc2i 12239	. . . . . . . . . . . . . 14 $/\$ $/\$
393	390, 391, 392	3imtr4i 281	. . . . . . . . . . . . 13 $/\$
394	393	adantll 750	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
395	372	rgen 2922	. . . . . . . . . . . 12
396		oveq2 6658	. . . . . . . . . . . . . . . . 17
397	396	oveq1d 6665	. . . . . . . . . . . . . . . 16
398		oveq1 6657	. . . . . . . . . . . . . . . 16
399	397, 398	oveq12d 6668	. . . . . . . . . . . . . . 15
400	399	eqeq2d 2632	. . . . . . . . . . . . . 14
401	400	ralbidv 2986	. . . . . . . . . . . . 13
402	401	rspcev 3309	. . . . . . . . . . . 12 $/\$
403	394, 395, 402	sylancl 694	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
404	280	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
405	185	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
406	188	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
407		brbtwn 25779	. . . . . . . . . . . 12 $/\$ $/\$
408	404, 405, 406, 407	syl3anc 1326	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
409	403, 408	mpbird 247	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
410	409	ex 450	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
411	386, 410	orim12d 883	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
412	283, 411	mpd 15	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $\/$
413		opeq2 4403	. . . . . . . . . 10
414	413	breq2d 4665	. . . . . . . . 9
415		breq1 4656	. . . . . . . . 9
416	414, 415	orbi12d 746	. . . . . . . 8 $\/$ $\/$
417	416, 5	elrab2 3366	. . . . . . 7 $/\$ $\/$
418	280, 412, 417	sylanbrc 698	. . . . . 6 $/\$ $/\$ $/\$ $/\$
419		fveq1 6190	. . . . . . . . 9
420	419	eqeq1d 2624	. . . . . . . 8
421	420	ralbidv 2986	. . . . . . 7
422	421	rspcev 3309	. . . . . 6 $/\$
423	418, 395, 422	sylancl 694	. . . . 5 $/\$ $/\$ $/\$ $/\$
424	6	simplbi 476	. . . . . . . . 9
425		ssrab2 3687	. . . . . . . . . . 11 $\/$
426	5, 425	eqsstri 3635	. . . . . . . . . 10
427	426	sseli 3599	. . . . . . . . 9
428	424, 427	anim12i 590	. . . . . . . 8 $/\$ $/\$
429		r19.26 3064	. . . . . . . . . 10 $/\$ $/\$
430		eqtr3 2643	. . . . . . . . . . 11 $/\$
431	430	ralimi 2952	. . . . . . . . . 10 $/\$
432	429, 431	sylbir 225	. . . . . . . . 9 $/\$
433		eqeefv 25783	. . . . . . . . . 10 $/\$
434	433	adantl 482	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
435	432, 434	syl5ibr 236	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
436	428, 435	sylan2 491	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
437	436	ralrimivva 2971	. . . . . 6 $/\$ $/\$ $/\$ $/\$
438	437	adantr 481	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$
439		df-reu 2919	. . . . . 6 $/\$
440		fveq1 6190	. . . . . . . . 9
441	440	eqeq1d 2624	. . . . . . . 8
442	441	ralbidv 2986	. . . . . . 7
443	442	reu4 3400	. . . . . 6 $/\$ $/\$
444	439, 443	bitr3i 266	. . . . 5 $/\$ $/\$ $/\$
445	423, 438, 444	sylanbrc 698	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$
446	445	ralrimiva 2966	. . 3 $/\$ $/\$ $/\$ $/\$
447		an12 838	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
448	447	opabbii 4717	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
449	257, 448	eqtri 2644	. . . . . 6 $/\$ $/\$
450	449	cnveqi 5297	. . . . 5 $/\$ $/\$
451		cnvopab 5533	. . . . 5 $/\$ $/\$ $/\$ $/\$
452	450, 451	eqtri 2644	. . . 4 $/\$ $/\$
453	452	fnopabg 6017	. . 3 $/\$
454	446, 453	sylib 208	. 2 $/\$ $/\$ $/\$
455		dff1o4 6145	. 2 $/\$
456	259, 454, 455	sylanbrc 698	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

weu 2470

wne 2794

wral 2912

wrex 2913

wreu 2914

crab 2916

wss 3574

cop 4183 class class class wbr 4653

copab 4712

cmpt 4729

ccnv 5113

wfn 5883

wf1o 5887

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

clt 10074

cle 10075

cmin 10266

cdiv 10684

cn 11020

cico 12177

cicc 12178

cfz 12326

cee 25768

cbtwn 25769

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-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

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-nel 2898 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-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-riota 6611 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-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-z 11378 df-uz 11688 df-ico 12181 df-icc 12182 df-fz 12327 df-ee 25771 df-btwn 25772

This theorem is referenced by: axcontlem5 25848 axcontlem9 25852 axcontlem10 25853

W3C validator