outpasch - Metamath Proof Explorer

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

Theorem outpasch 24790

Description: Axiom of Pasch, outer form. This was proven by Gupta from other axioms and is therefore presented as Theorem 9.6 in [Schwabhauser] p. 70. (Contributed by Thierry Arnoux, 16-Aug-2020.)

**Hypotheses**
Ref	Expression
outpasch.p
outpasch.i	Itv
outpasch.l	LineG
outpasch.g	TarskiG
outpasch.a
outpasch.b
outpasch.c
outpasch.r
outpasch.q
outpasch.1
outpasch.2

**Assertion**
Ref	Expression
outpasch	$/\$

Distinct variable groups:

Proof of Theorem outpasch Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		outpasch.a	. . . . . 6
2	1	adantr 467	. . . . 5 $/\$
3		simpr 463	. . . . . . 7 $/\$ $/\$
4	3	eleq1d 2512	. . . . . 6 $/\$ $/\$
5	3	oveq2d 6304	. . . . . . 7 $/\$ $/\$
6	5	eleq2d 2513	. . . . . 6 $/\$ $/\$
7	4, 6	anbi12d 716	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		outpasch.p	. . . . . . . 8
9		eqid 2450	. . . . . . . 8
10		outpasch.i	. . . . . . . 8 Itv
11		outpasch.g	. . . . . . . 8 TarskiG
12		outpasch.b	. . . . . . . 8
13	8, 9, 10, 11, 1, 12	tgbtwntriv1 24528	. . . . . . 7
14	13	adantr 467	. . . . . 6 $/\$
15	11	adantr 467	. . . . . . 7 $/\$ TarskiG
16		outpasch.r	. . . . . . . 8
17	16	adantr 467	. . . . . . 7 $/\$
18		outpasch.q	. . . . . . . 8
19	18	adantr 467	. . . . . . 7 $/\$
20		outpasch.c	. . . . . . . 8
21	20	adantr 467	. . . . . . 7 $/\$
22		simpr 463	. . . . . . 7 $/\$
23		outpasch.1	. . . . . . . . 9
24	8, 9, 10, 11, 1, 20, 16, 23	tgbtwncom 24525	. . . . . . . 8
25	24	adantr 467	. . . . . . 7 $/\$
26	8, 9, 10, 15, 17, 19, 21, 2, 22, 25	tgbtwnexch 24535	. . . . . 6 $/\$
27	14, 26	jca 535	. . . . 5 $/\$ $/\$
28	2, 7, 27	rspcedvd 3154	. . . 4 $/\$ $/\$
29	28	adantlr 720	. . 3 $/\$ $\/$ $/\$ $/\$
30	12	ad2antrr 731	. . . 4 $/\$ $\/$ $/\$
31		eleq1 2516	. . . . . 6
32		eqidd 2451	. . . . . . 7
33		oveq2 6296	. . . . . . 7
34	32, 33	eleq12d 2522	. . . . . 6
35	31, 34	anbi12d 716	. . . . 5 $/\$ $/\$
36	35	adantl 468	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
37	8, 9, 10, 11, 1, 12	tgbtwntriv2 24524	. . . . . 6
38	37	ad2antrr 731	. . . . 5 $/\$ $\/$ $/\$
39	11	ad2antrr 731	. . . . . . . 8 $/\$ $\/$ $/\$ TarskiG
40	39	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ TarskiG
41	20	ad3antrrr 735	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
42	16	ad3antrrr 735	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
43	18	ad3antrrr 735	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
44	30	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
45		simpr 463	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
46	8, 9, 10, 40, 43, 42, 41, 45	tgbtwncom 24525	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
47		outpasch.2	. . . . . . . . 9
48	8, 9, 10, 11, 12, 18, 20, 47	tgbtwncom 24525	. . . . . . . 8
49	48	ad3antrrr 735	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
50	8, 9, 10, 40, 41, 42, 43, 44, 46, 49	tgbtwnexch3 24531	. . . . . 6 $/\$ $\/$ $/\$ $/\$
51	39	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ TarskiG
52	30	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
53	18	ad3antrrr 735	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
54	16	ad3antrrr 735	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
55	20	ad3antrrr 735	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
56		simpr 463	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
57	8, 9, 10, 11, 16, 20	tgbtwntriv2 24524	. . . . . . . . . . . 12
58	57	ad4antr 737	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
59	56, 58	eqeltrd 2528	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
60		simpllr 768	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
61	59, 60	pm2.65da 579	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$
62	61	neqned 2630	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
63	47	ad3antrrr 735	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
64		simpr 463	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
65	8, 9, 10, 51, 52, 53, 55, 54, 62, 63, 64	tgbtwnouttr 24534	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
66	8, 9, 10, 51, 52, 53, 54, 65	tgbtwncom 24525	. . . . . 6 $/\$ $\/$ $/\$ $/\$
67		outpasch.l	. . . . . . . . . . 11 LineG
68	8, 67, 10, 11, 18, 20, 16	tgcolg 24592	. . . . . . . . . 10 $\/$ $\/$ $\/$
69	68	biimpa 487	. . . . . . . . 9 $/\$ $\/$ $\/$ $\/$
70		3orcoma 992	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
71		3orass 987	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
72	70, 71	bitr3i 255	. . . . . . . . 9 $\/$ $\/$ $\/$ $\/$
73	69, 72	sylib 200	. . . . . . . 8 $/\$ $\/$ $\/$ $\/$
74	73	ord 379	. . . . . . 7 $/\$ $\/$ $\/$
75	74	imp 431	. . . . . 6 $/\$ $\/$ $/\$ $\/$
76	50, 66, 75	mpjaodan 794	. . . . 5 $/\$ $\/$ $/\$
77	38, 76	jca 535	. . . 4 $/\$ $\/$ $/\$ $/\$
78	30, 36, 77	rspcedvd 3154	. . 3 $/\$ $\/$ $/\$ $/\$
79	29, 78	pm2.61dan 799	. 2 $/\$ $\/$ $/\$
80	12	ad2antrr 731	. . . 4 $/\$ $\/$ $/\$
81	35	adantl 468	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
82	37	ad2antrr 731	. . . . 5 $/\$ $\/$ $/\$
83	11	ad2antrr 731	. . . . . . 7 $/\$ $\/$ $/\$ TarskiG
84	16	ad2antrr 731	. . . . . . 7 $/\$ $\/$ $/\$
85	18	ad2antrr 731	. . . . . . 7 $/\$ $\/$ $/\$
86	20	ad2antrr 731	. . . . . . 7 $/\$ $\/$ $/\$
87		simplr 761	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
88		simpr 463	. . . . . . 7 $/\$ $\/$ $/\$
89	11	adantr 467	. . . . . . . . 9 $/\$ $\/$ TarskiG
90	16	adantr 467	. . . . . . . . 9 $/\$ $\/$
91	18	adantr 467	. . . . . . . . 9 $/\$ $\/$
92	20	adantr 467	. . . . . . . . . 10 $/\$ $\/$
93		simpr 463	. . . . . . . . . 10 $/\$ $\/$ $\/$
94	8, 10, 67, 89, 90, 91, 92, 93	ncolne1 24663	. . . . . . . . 9 $/\$ $\/$
95	8, 10, 67, 89, 90, 91, 94	tglinerflx2 24672	. . . . . . . 8 $/\$ $\/$
96	95	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$
97	8, 67, 10, 89, 91, 92, 90, 93	ncolcom 24599	. . . . . . . . . . 11 $/\$ $\/$ $\/$
98	8, 67, 10, 89, 92, 91, 90, 97	ncolrot1 24600	. . . . . . . . . 10 $/\$ $\/$ $\/$
99	8, 10, 67, 89, 92, 91, 90, 98	ncolne1 24663	. . . . . . . . 9 $/\$ $\/$
100	99	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$
101	48	ad2antrr 731	. . . . . . . 8 $/\$ $\/$ $/\$
102	8, 10, 67, 83, 86, 85, 80, 100, 101	btwnlng3 24659	. . . . . . 7 $/\$ $\/$ $/\$
103	8, 10, 67, 83, 86, 85, 100	tglinerflx2 24672	. . . . . . 7 $/\$ $\/$ $/\$
104	8, 10, 67, 83, 84, 85, 86, 85, 87, 88, 96, 102, 103	tglineinteq 24683	. . . . . 6 $/\$ $\/$ $/\$
105	8, 9, 10, 11, 16, 12	tgbtwntriv2 24524	. . . . . . 7
106	105	ad2antrr 731	. . . . . 6 $/\$ $\/$ $/\$
107	104, 106	eqeltrrd 2529	. . . . 5 $/\$ $\/$ $/\$
108	82, 107	jca 535	. . . 4 $/\$ $\/$ $/\$ $/\$
109	80, 81, 108	rspcedvd 3154	. . 3 $/\$ $\/$ $/\$ $/\$
110		eleq1 2516	. . . . . . . . . 10
111	110	cbvrexv 3019	. . . . . . . . 9
112	111	anbi2i 699	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
113	112	opabbii 4466	. . . . . . 7 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
114	89	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$ TarskiG
115	90	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$
116	91	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$
117	94	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$
118	8, 10, 67, 114, 115, 116, 117	tgelrnln 24668	. . . . . . 7 $/\$ $\/$ $/\$
119		eqid 2450	. . . . . . 7 hlG hlG
120	20	ad2antrr 731	. . . . . . 7 $/\$ $\/$ $/\$
121	1	ad2antrr 731	. . . . . . 7 $/\$ $\/$ $/\$
122	12	adantr 467	. . . . . . . 8 $/\$ $\/$
123	122	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$
124	95	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$
125	8, 67, 10, 89, 91, 92, 90, 93	ncolrot2 24601	. . . . . . . . . 10 $/\$ $\/$ $\/$
126		pm2.45 399	. . . . . . . . . 10 $\/$
127	125, 126	syl 17	. . . . . . . . 9 $/\$ $\/$
128	127	adantr 467	. . . . . . . 8 $/\$ $\/$ $/\$
129		simpr 463	. . . . . . . 8 $/\$ $\/$ $/\$
130	48	ad2antrr 731	. . . . . . . 8 $/\$ $\/$ $/\$
131	8, 9, 10, 113, 120, 123, 124, 128, 129, 130	islnoppd 24775	. . . . . . 7 $/\$ $\/$ $/\$ $\$ $/\$ $\$ $/\$
132	8, 10, 67, 89, 90, 91, 94	tglinerflx1 24671	. . . . . . . 8 $/\$ $\/$
133	132	adantr 467	. . . . . . 7 $/\$ $\/$ $/\$
134	23	ad2antrr 731	. . . . . . . 8 $/\$ $\/$ $/\$
135	24	ad2antrr 731	. . . . . . . . . 10 $/\$ $\/$ $/\$
136	8, 10, 67, 89, 92, 90, 91, 125	ncolne1 24663	. . . . . . . . . . 11 $/\$ $\/$
137	136	adantr 467	. . . . . . . . . 10 $/\$ $\/$ $/\$
138	8, 9, 10, 114, 115, 120, 121, 135, 137	tgbtwnne 24527	. . . . . . . . 9 $/\$ $\/$ $/\$
139	138	necomd 2678	. . . . . . . 8 $/\$ $\/$ $/\$
140	8, 10, 119, 121, 115, 120, 114, 121, 134, 139, 137	btwnhl2 24651	. . . . . . 7 $/\$ $\/$ $/\$ hlG
141	8, 9, 10, 113, 67, 118, 114, 119, 120, 121, 123, 131, 133, 140	opphl 24789	. . . . . 6 $/\$ $\/$ $/\$ $\$ $/\$ $\$ $/\$
142	8, 9, 10, 113, 121, 123	islnopp 24774	. . . . . 6 $/\$ $\/$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
143	141, 142	mpbid 214	. . . . 5 $/\$ $\/$ $/\$ $/\$ $/\$
144	143	simprd 465	. . . 4 $/\$ $\/$ $/\$
145	114	ad2antrr 731	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ TarskiG
146	118	ad2antrr 731	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
147		simplr 761	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
148	8, 67, 10, 145, 146, 147	tglnpt 24587	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
149		simpr 463	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
150	145	ad2antrr 731	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ TarskiG
151	90	ad3antrrr 735	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
152	151	ad2antrr 731	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153	91	ad5antr 739	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154	120	ad2antrr 731	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
155	154	ad2antrr 731	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156	93	ad5antr 739	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
157		simplr 761	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	117	ad4antr 737	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
159	148	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160	94	necomd 2678	. . . . . . . . . . . . . . 15 $/\$ $\/$
161	160	ad5antr 739	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	147	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	8, 10, 67, 150, 153, 152, 159, 161, 162	lncom 24660	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164		simprl 763	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165	8, 10, 67, 150, 159, 153, 152, 157, 163, 164	coltr3 24686	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	8, 10, 67, 150, 152, 153, 157, 158, 165	lncom 24660	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	95	ad5antr 739	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	99	ad5antr 739	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169	123	ad2antrr 731	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$
170	169	ad2antrr 731	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
171	99	necomd 2678	. . . . . . . . . . . . . . 15 $/\$ $\/$
172	47	adantr 467	. . . . . . . . . . . . . . 15 $/\$ $\/$
173	8, 10, 67, 89, 91, 92, 122, 171, 172	btwnlng2 24658	. . . . . . . . . . . . . 14 $/\$ $\/$
174	173	ad5antr 739	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175		simprr 765	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	8, 9, 10, 150, 155, 157, 170, 175	tgbtwncom 24525	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	8, 10, 67, 150, 170, 153, 155, 157, 174, 176	coltr3 24686	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178	8, 10, 67, 150, 155, 153, 157, 168, 177	lncom 24660	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179	8, 10, 67, 89, 92, 91, 99	tglinerflx2 24672	. . . . . . . . . . . 12 $/\$ $\/$
180	179	ad5antr 739	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	8, 10, 67, 150, 152, 153, 155, 153, 156, 166, 167, 178, 180	tglineinteq 24683	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	8, 9, 10, 150, 159, 157, 152, 164	tgbtwncom 24525	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	181, 182	eqeltrrd 2529	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184	121	ad2antrr 731	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
185	8, 9, 10, 145, 184, 148, 169, 149	tgbtwncom 24525	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
186	24	ad4antr 737	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
187	8, 9, 10, 145, 169, 151, 184, 148, 154, 185, 186	axtgpasch 24508	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
188	183, 187	r19.29a 2931	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
189	148, 149, 188	jca32 538	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
190	189	anasss 652	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
191	190	ex 436	. . . . 5 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
192	191	reximdv2 2857	. . . 4 $/\$ $\/$ $/\$ $/\$
193	144, 192	mpd 15	. . 3 $/\$ $\/$ $/\$ $/\$
194	109, 193	pm2.61dan 799	. 2 $/\$ $\/$ $/\$
195	79, 194	pm2.61dan 799	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $\/$ wo 370 $/\$ wa 371 $\/$ w3o 983

wceq 1443

wcel 1886

wne 2621

wrex 2737 $\$ cdif 3400 class class class wbr 4401

copab 4459

crn 4834

cfv 5581 (class class class)co 6288

cbs 15114

cds 15192 TarskiGcstrkg 24471 Itvcitv 24477 LineGclng 24478 hlGchlg 24638

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-oadd 7183 df-er 7360 df-map 7471 df-pm 7472 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-card 8370 df-cda 8595 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-fz 11782 df-fzo 11913 df-hash 12513 df-word 12661 df-concat 12663 df-s1 12664 df-s2 12939 df-s3 12940 df-trkgc 24489 df-trkgb 24490 df-trkgcb 24491 df-trkgld 24493 df-trkg 24494 df-cgrg 24549 df-leg 24621 df-hlg 24639 df-mir 24691 df-rag 24732 df-perpg 24734

This theorem is referenced by: hlpasch 24791

W3C validator