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 24876

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 472	. . . . 5 $/\$
3		simpr 468	. . . . . . 7 $/\$ $/\$
4	3	eleq1d 2533	. . . . . 6 $/\$ $/\$
5	3	oveq2d 6324	. . . . . . 7 $/\$ $/\$
6	5	eleq2d 2534	. . . . . 6 $/\$ $/\$
7	4, 6	anbi12d 725	. . . . 5 $/\$ $/\$ $/\$ $/\$
8		outpasch.p	. . . . . . . 8
9		eqid 2471	. . . . . . . 8
10		outpasch.i	. . . . . . . 8 Itv
11		outpasch.g	. . . . . . . 8 TarskiG
12		outpasch.b	. . . . . . . 8
13	8, 9, 10, 11, 1, 12	tgbtwntriv1 24614	. . . . . . 7
14	13	adantr 472	. . . . . 6 $/\$
15	11	adantr 472	. . . . . . 7 $/\$ TarskiG
16		outpasch.r	. . . . . . . 8
17	16	adantr 472	. . . . . . 7 $/\$
18		outpasch.q	. . . . . . . 8
19	18	adantr 472	. . . . . . 7 $/\$
20		outpasch.c	. . . . . . . 8
21	20	adantr 472	. . . . . . 7 $/\$
22		simpr 468	. . . . . . 7 $/\$
23		outpasch.1	. . . . . . . . 9
24	8, 9, 10, 11, 1, 20, 16, 23	tgbtwncom 24611	. . . . . . . 8
25	24	adantr 472	. . . . . . 7 $/\$
26	8, 9, 10, 15, 17, 19, 21, 2, 22, 25	tgbtwnexch 24621	. . . . . 6 $/\$
27	14, 26	jca 541	. . . . 5 $/\$ $/\$
28	2, 7, 27	rspcedvd 3143	. . . 4 $/\$ $/\$
29	28	adantlr 729	. . 3 $/\$ $\/$ $/\$ $/\$
30	12	ad2antrr 740	. . . 4 $/\$ $\/$ $/\$
31		eleq1 2537	. . . . . 6
32		eqidd 2472	. . . . . . 7
33		oveq2 6316	. . . . . . 7
34	32, 33	eleq12d 2543	. . . . . 6
35	31, 34	anbi12d 725	. . . . 5 $/\$ $/\$
36	35	adantl 473	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
37	8, 9, 10, 11, 1, 12	tgbtwntriv2 24610	. . . . . 6
38	37	ad2antrr 740	. . . . 5 $/\$ $\/$ $/\$
39	11	ad2antrr 740	. . . . . . . 8 $/\$ $\/$ $/\$ TarskiG
40	39	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ TarskiG
41	20	ad3antrrr 744	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
42	16	ad3antrrr 744	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
43	18	ad3antrrr 744	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
44	30	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
45		simpr 468	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
46	8, 9, 10, 40, 43, 42, 41, 45	tgbtwncom 24611	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
47		outpasch.2	. . . . . . . . 9
48	8, 9, 10, 11, 12, 18, 20, 47	tgbtwncom 24611	. . . . . . . 8
49	48	ad3antrrr 744	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
50	8, 9, 10, 40, 41, 42, 43, 44, 46, 49	tgbtwnexch3 24617	. . . . . 6 $/\$ $\/$ $/\$ $/\$
51	39	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ TarskiG
52	30	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
53	18	ad3antrrr 744	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
54	16	ad3antrrr 744	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
55	20	ad3antrrr 744	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
56		simpr 468	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
57	8, 9, 10, 11, 16, 20	tgbtwntriv2 24610	. . . . . . . . . . . 12
58	57	ad4antr 746	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$
59	56, 58	eqeltrd 2549	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
60		simpllr 777	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
61	59, 60	pm2.65da 586	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$
62	61	neqned 2650	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
63	47	ad3antrrr 744	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
64		simpr 468	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$
65	8, 9, 10, 51, 52, 53, 55, 54, 62, 63, 64	tgbtwnouttr 24620	. . . . . . 7 $/\$ $\/$ $/\$ $/\$
66	8, 9, 10, 51, 52, 53, 54, 65	tgbtwncom 24611	. . . . . 6 $/\$ $\/$ $/\$ $/\$
67		outpasch.l	. . . . . . . . . . 11 LineG
68	8, 67, 10, 11, 18, 20, 16	tgcolg 24678	. . . . . . . . . 10 $\/$ $\/$ $\/$
69	68	biimpa 492	. . . . . . . . 9 $/\$ $\/$ $\/$ $\/$
70		3orcoma 1015	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
71		3orass 1010	. . . . . . . . . 10 $\/$ $\/$ $\/$ $\/$
72	70, 71	bitr3i 259	. . . . . . . . 9 $\/$ $\/$ $\/$ $\/$
73	69, 72	sylib 201	. . . . . . . 8 $/\$ $\/$ $\/$ $\/$
74	73	ord 384	. . . . . . 7 $/\$ $\/$ $\/$
75	74	imp 436	. . . . . 6 $/\$ $\/$ $/\$ $\/$
76	50, 66, 75	mpjaodan 803	. . . . 5 $/\$ $\/$ $/\$
77	38, 76	jca 541	. . . 4 $/\$ $\/$ $/\$ $/\$
78	30, 36, 77	rspcedvd 3143	. . 3 $/\$ $\/$ $/\$ $/\$
79	29, 78	pm2.61dan 808	. 2 $/\$ $\/$ $/\$
80	12	ad2antrr 740	. . . 4 $/\$ $\/$ $/\$
81	35	adantl 473	. . . 4 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
82	37	ad2antrr 740	. . . . 5 $/\$ $\/$ $/\$
83	11	ad2antrr 740	. . . . . . 7 $/\$ $\/$ $/\$ TarskiG
84	16	ad2antrr 740	. . . . . . 7 $/\$ $\/$ $/\$
85	18	ad2antrr 740	. . . . . . 7 $/\$ $\/$ $/\$
86	20	ad2antrr 740	. . . . . . 7 $/\$ $\/$ $/\$
87		simplr 770	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
88		simpr 468	. . . . . . 7 $/\$ $\/$ $/\$
89	11	adantr 472	. . . . . . . . 9 $/\$ $\/$ TarskiG
90	16	adantr 472	. . . . . . . . 9 $/\$ $\/$
91	18	adantr 472	. . . . . . . . 9 $/\$ $\/$
92	20	adantr 472	. . . . . . . . . 10 $/\$ $\/$
93		simpr 468	. . . . . . . . . 10 $/\$ $\/$ $\/$
94	8, 10, 67, 89, 90, 91, 92, 93	ncolne1 24749	. . . . . . . . 9 $/\$ $\/$
95	8, 10, 67, 89, 90, 91, 94	tglinerflx2 24758	. . . . . . . 8 $/\$ $\/$
96	95	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$
97	8, 67, 10, 89, 91, 92, 90, 93	ncolcom 24685	. . . . . . . . . . 11 $/\$ $\/$ $\/$
98	8, 67, 10, 89, 92, 91, 90, 97	ncolrot1 24686	. . . . . . . . . 10 $/\$ $\/$ $\/$
99	8, 10, 67, 89, 92, 91, 90, 98	ncolne1 24749	. . . . . . . . 9 $/\$ $\/$
100	99	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$
101	48	ad2antrr 740	. . . . . . . 8 $/\$ $\/$ $/\$
102	8, 10, 67, 83, 86, 85, 80, 100, 101	btwnlng3 24745	. . . . . . 7 $/\$ $\/$ $/\$
103	8, 10, 67, 83, 86, 85, 100	tglinerflx2 24758	. . . . . . 7 $/\$ $\/$ $/\$
104	8, 10, 67, 83, 84, 85, 86, 85, 87, 88, 96, 102, 103	tglineinteq 24769	. . . . . 6 $/\$ $\/$ $/\$
105	8, 9, 10, 11, 16, 12	tgbtwntriv2 24610	. . . . . . 7
106	105	ad2antrr 740	. . . . . 6 $/\$ $\/$ $/\$
107	104, 106	eqeltrrd 2550	. . . . 5 $/\$ $\/$ $/\$
108	82, 107	jca 541	. . . 4 $/\$ $\/$ $/\$ $/\$
109	80, 81, 108	rspcedvd 3143	. . 3 $/\$ $\/$ $/\$ $/\$
110		eleq1 2537	. . . . . . . . . 10
111	110	cbvrexv 3006	. . . . . . . . 9
112	111	anbi2i 708	. . . . . . . 8 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
113	112	opabbii 4460	. . . . . . 7 $\$ $/\$ $\$ $/\$ $\$ $/\$ $\$ $/\$
114	89	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$ TarskiG
115	90	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$
116	91	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$
117	94	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$
118	8, 10, 67, 114, 115, 116, 117	tgelrnln 24754	. . . . . . 7 $/\$ $\/$ $/\$
119		eqid 2471	. . . . . . 7 hlG hlG
120	20	ad2antrr 740	. . . . . . 7 $/\$ $\/$ $/\$
121	1	ad2antrr 740	. . . . . . 7 $/\$ $\/$ $/\$
122	12	adantr 472	. . . . . . . 8 $/\$ $\/$
123	122	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$
124	95	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$
125	8, 67, 10, 89, 91, 92, 90, 93	ncolrot2 24687	. . . . . . . . . 10 $/\$ $\/$ $\/$
126		pm2.45 404	. . . . . . . . . 10 $\/$
127	125, 126	syl 17	. . . . . . . . 9 $/\$ $\/$
128	127	adantr 472	. . . . . . . 8 $/\$ $\/$ $/\$
129		simpr 468	. . . . . . . 8 $/\$ $\/$ $/\$
130	48	ad2antrr 740	. . . . . . . 8 $/\$ $\/$ $/\$
131	8, 9, 10, 113, 120, 123, 124, 128, 129, 130	islnoppd 24861	. . . . . . 7 $/\$ $\/$ $/\$ $\$ $/\$ $\$ $/\$
132	8, 10, 67, 89, 90, 91, 94	tglinerflx1 24757	. . . . . . . 8 $/\$ $\/$
133	132	adantr 472	. . . . . . 7 $/\$ $\/$ $/\$
134	23	ad2antrr 740	. . . . . . . 8 $/\$ $\/$ $/\$
135	24	ad2antrr 740	. . . . . . . . . 10 $/\$ $\/$ $/\$
136	8, 10, 67, 89, 92, 90, 91, 125	ncolne1 24749	. . . . . . . . . . 11 $/\$ $\/$
137	136	adantr 472	. . . . . . . . . 10 $/\$ $\/$ $/\$
138	8, 9, 10, 114, 115, 120, 121, 135, 137	tgbtwnne 24613	. . . . . . . . 9 $/\$ $\/$ $/\$
139	138	necomd 2698	. . . . . . . 8 $/\$ $\/$ $/\$
140	8, 10, 119, 121, 115, 120, 114, 121, 134, 139, 137	btwnhl2 24737	. . . . . . 7 $/\$ $\/$ $/\$ hlG
141	8, 9, 10, 113, 67, 118, 114, 119, 120, 121, 123, 131, 133, 140	opphl 24875	. . . . . 6 $/\$ $\/$ $/\$ $\$ $/\$ $\$ $/\$
142	8, 9, 10, 113, 121, 123	islnopp 24860	. . . . . 6 $/\$ $\/$ $/\$ $\$ $/\$ $\$ $/\$ $/\$ $/\$
143	141, 142	mpbid 215	. . . . 5 $/\$ $\/$ $/\$ $/\$ $/\$
144	143	simprd 470	. . . 4 $/\$ $\/$ $/\$
145	114	ad2antrr 740	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ TarskiG
146	118	ad2antrr 740	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
147		simplr 770	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$
148	8, 67, 10, 145, 146, 147	tglnpt 24673	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
149		simpr 468	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
150	145	ad2antrr 740	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ TarskiG
151	90	ad3antrrr 744	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
152	151	ad2antrr 740	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
153	91	ad5antr 748	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
154	120	ad2antrr 740	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$
155	154	ad2antrr 740	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
156	93	ad5antr 748	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$
157		simplr 770	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
158	117	ad4antr 746	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
159	148	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160	94	necomd 2698	. . . . . . . . . . . . . . 15 $/\$ $\/$
161	160	ad5antr 748	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	147	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	8, 10, 67, 150, 153, 152, 159, 161, 162	lncom 24746	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164		simprl 772	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
165	8, 10, 67, 150, 159, 153, 152, 157, 163, 164	coltr3 24772	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
166	8, 10, 67, 150, 152, 153, 157, 158, 165	lncom 24746	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
167	95	ad5antr 748	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
168	99	ad5antr 748	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
169	123	ad2antrr 740	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$
170	169	ad2antrr 740	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
171	99	necomd 2698	. . . . . . . . . . . . . . 15 $/\$ $\/$
172	47	adantr 472	. . . . . . . . . . . . . . 15 $/\$ $\/$
173	8, 10, 67, 89, 91, 92, 122, 171, 172	btwnlng2 24744	. . . . . . . . . . . . . 14 $/\$ $\/$
174	173	ad5antr 748	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
175		simprr 774	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
176	8, 9, 10, 150, 155, 157, 170, 175	tgbtwncom 24611	. . . . . . . . . . . . 13 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
177	8, 10, 67, 150, 170, 153, 155, 157, 174, 176	coltr3 24772	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
178	8, 10, 67, 150, 155, 153, 157, 168, 177	lncom 24746	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
179	8, 10, 67, 89, 92, 91, 99	tglinerflx2 24758	. . . . . . . . . . . 12 $/\$ $\/$
180	179	ad5antr 748	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
181	8, 10, 67, 150, 152, 153, 155, 153, 156, 166, 167, 178, 180	tglineinteq 24769	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
182	8, 9, 10, 150, 159, 157, 152, 164	tgbtwncom 24611	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
183	181, 182	eqeltrrd 2550	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
184	121	ad2antrr 740	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
185	8, 9, 10, 145, 184, 148, 169, 149	tgbtwncom 24611	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
186	24	ad4antr 746	. . . . . . . . . 10 $/\$ $\/$ $/\$ $/\$ $/\$
187	8, 9, 10, 145, 169, 151, 184, 148, 154, 185, 186	axtgpasch 24594	. . . . . . . . 9 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
188	183, 187	r19.29a 2918	. . . . . . . 8 $/\$ $\/$ $/\$ $/\$ $/\$
189	148, 149, 188	jca32 544	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
190	189	anasss 659	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$ $/\$
191	190	ex 441	. . . . 5 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
192	191	reximdv2 2855	. . . 4 $/\$ $\/$ $/\$ $/\$
193	144, 192	mpd 15	. . 3 $/\$ $\/$ $/\$ $/\$
194	109, 193	pm2.61dan 808	. 2 $/\$ $\/$ $/\$
195	79, 194	pm2.61dan 808	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 375 $/\$ wa 376 $\/$ w3o 1006

wceq 1452

wcel 1904

wne 2641

wrex 2757 $\$ cdif 3387 class class class wbr 4395

copab 4453

crn 4840

cfv 5589 (class class class)co 6308

cbs 15199

cds 15277 TarskiGcstrkg 24557 Itvcitv 24563 LineGclng 24564 hlGchlg 24724

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-int 4227 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-oadd 7204 df-er 7381 df-map 7492 df-pm 7493 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-card 8391 df-cda 8616 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-2 10690 df-3 10691 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-fzo 11943 df-hash 12554 df-word 12711 df-concat 12713 df-s1 12714 df-s2 13003 df-s3 13004 df-trkgc 24575 df-trkgb 24576 df-trkgcb 24577 df-trkgld 24579 df-trkg 24580 df-cgrg 24635 df-leg 24707 df-hlg 24725 df-mir 24777 df-rag 24818 df-perpg 24820

This theorem is referenced by: hlpasch 24877

W3C validator