numclwwlkovf2exlem2 - Metamath Proof Explorer

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

Theorem numclwwlkovf2exlem2 27212

Description: Lemma 2 for numclwwlkovf2ex 27219: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.)

**Hypotheses**
Ref	Expression
numclwwlkovf2exlem2.v	Vtx
numclwwlkovf2exlem2.e	Edg

**Assertion**
Ref	Expression
numclwwlkovf2exlem2	USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ..^ ++ ++ ++ ++

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

**Proof of Theorem numclwwlkovf2exlem2**
Step	Hyp	Ref	Expression
1		numclwwlkovf2exlem2.v	. . . . . . . . 9 Vtx
2	1	nbgrisvtx 26255	. . . . . . . 8 USGraph $/\$ NeighbVtx
3		simpll 790	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ ..^ Word
4		elfzonn0 12512	. . . . . . . . . . . . . . . . . . . . 21 ..^
5	4	adantl 482	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ ..^
6		lencl 13324	. . . . . . . . . . . . . . . . . . . . . . 23 Word
7		elfzo0 12508	. . . . . . . . . . . . . . . . . . . . . . . 24 ..^ $/\$ $/\$
8		nn0re 11301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9	8	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
10		nn0re 11301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
11		peano2rem 10348	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
12	10, 11	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
13	12	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
14	10	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
15	9, 13, 14	3jca 1242	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
16	10	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
17	16	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
18		lttr 10114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$
19	18	expcomd 454	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
20	15, 17, 19	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
21	20	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
22	21	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
23	7, 22	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
24	6, 23	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 Word ..^
25	24	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ ..^
26	25	imp 445	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ ..^
27		simplr 792	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ ..^ $/\$
28		ccat2s1fvw 13415	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ $/\$ ++ ++
29	3, 5, 26, 27, 28	syl31anc 1329	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ..^ ++ ++
30	29	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ $/\$ ..^ ++ ++
31		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ ..^ Word
32		peano2nn0 11333	. . . . . . . . . . . . . . . . . . . . . . . . 25
33	32	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
34	7, 33	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
35	34	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ ..^
36		1red 10055	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
37	9, 36, 14	ltaddsubd 10627	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
38	37	biimprd 238	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
39	38	impancom 456	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
40	39	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
41	7, 40	sylbi 207	. . . . . . . . . . . . . . . . . . . . . . 23 ..^
42	6, 41	mpan9 486	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ ..^
43	31, 35, 42	3jca 1242	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ ..^ Word $/\$ $/\$
44	43	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ ..^ Word $/\$ $/\$
45		ccat2s1fvw 13415	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ $/\$ $/\$ ++ ++
46	44, 27, 45	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 Word $/\$ $/\$ $/\$ ..^ ++ ++
47	46	eqcomd 2628	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ $/\$ ..^ ++ ++
48	30, 47	preq12d 4276	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ $/\$ ..^ ++ ++ ++ ++
49	48	eleq1d 2686	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ ..^ ++ ++ ++ ++
50	49	ralbidva 2985	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ ..^ ..^ ++ ++ ++ ++
51	50	biimpd 219	. . . . . . . . . . . . . 14 Word $/\$ $/\$ ..^ ..^ ++ ++ ++ ++
52	51	impancom 456	. . . . . . . . . . . . 13 Word $/\$ ..^ $/\$ ..^ ++ ++ ++ ++
53	52	3adant3 1081	. . . . . . . . . . . 12 Word $/\$ ..^ $/\$ lastS $/\$ ..^ ++ ++ ++ ++
54	53	3ad2ant1 1082	. . . . . . . . . . 11 Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ ..^ ++ ++ ++ ++
55	54	com12 32	. . . . . . . . . 10 $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ ..^ ++ ++ ++ ++
56	55	expcom 451	. . . . . . . . 9 Word $/\$ ..^ $/\$ lastS $/\$ $/\$ ..^ ++ ++ ++ ++
57	56	com23 86	. . . . . . . 8 Word $/\$ ..^ $/\$ lastS $/\$ $/\$ ..^ ++ ++ ++ ++
58	2, 57	syl 17	. . . . . . 7 USGraph $/\$ NeighbVtx Word $/\$ ..^ $/\$ lastS $/\$ $/\$ ..^ ++ ++ ++ ++
59	58	ex 450	. . . . . 6 USGraph NeighbVtx Word $/\$ ..^ $/\$ lastS $/\$ $/\$ ..^ ++ ++ ++ ++
60	59	com24 95	. . . . 5 USGraph Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx ..^ ++ ++ ++ ++
61	60	imp 445	. . . 4 USGraph $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx ..^ ++ ++ ++ ++
62	61	3adant3 1081	. . 3 USGraph $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx ..^ ++ ++ ++ ++
63	62	imp31 448	. 2 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ..^ ++ ++ ++ ++
64	2	ex 450	. . . . . . . . . . . . 13 USGraph NeighbVtx
65	64	adantr 481	. . . . . . . . . . . 12 USGraph $/\$ NeighbVtx
66		simpr 477	. . . . . . . . . . . 12 USGraph $/\$
67	65, 66	jctild 566	. . . . . . . . . . 11 USGraph $/\$ NeighbVtx $/\$
68	67	3adant3 1081	. . . . . . . . . 10 USGraph $/\$ $/\$ NeighbVtx $/\$
69		simpl 473	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$ Word
70		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . 25
71	70	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
72		eluzelcn 11699	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
73		2cnd 11093	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
74		1cnd 10056	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
75	72, 73, 74	subsub4d 10423	. . . . . . . . . . . . . . . . . . . . . . . . . 26
76		2p1e3 11151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
77	76	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
78	77	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
79		uznn0sub 11719	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
80	78, 79	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . . 26
81	75, 80	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . . . 25
82	81	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
83	71, 82	eqeltrd 2701	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
84	83	ancoms 469	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
85	84	adantl 482	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$
86	6, 10	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 Word
87	86	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$
88	87	ltm1d 10956	. . . . . . . . . . . . . . . . . . . . 21 Word $/\$ $/\$
89	69, 85, 88	3jca 1242	. . . . . . . . . . . . . . . . . . . 20 Word $/\$ $/\$ Word $/\$ $/\$
90	89	ex 450	. . . . . . . . . . . . . . . . . . 19 Word $/\$ Word $/\$ $/\$
91	90	adantr 481	. . . . . . . . . . . . . . . . . 18 Word $/\$ lastS $/\$ Word $/\$ $/\$
92	91	3ad2ant1 1082	. . . . . . . . . . . . . . . . 17 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
93	92	imp 445	. . . . . . . . . . . . . . . 16 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$ Word $/\$ $/\$
94		simpl2 1065	. . . . . . . . . . . . . . . 16 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
95		ccat2s1fvw 13415	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ $/\$ $/\$ ++ ++
96	93, 94, 95	syl2anc 693	. . . . . . . . . . . . . . 15 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$ ++ ++
97		nn0cn 11302	. . . . . . . . . . . . . . . . . . . . . 22
98		ax-1cn 9994	. . . . . . . . . . . . . . . . . . . . . 22
99		npcan 10290	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
100	97, 98, 99	sylancl 694	. . . . . . . . . . . . . . . . . . . . 21
101	6, 100	syl 17	. . . . . . . . . . . . . . . . . . . 20 Word
102	101	adantr 481	. . . . . . . . . . . . . . . . . . 19 Word $/\$ lastS
103	102	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 Word $/\$ lastS $/\$ $/\$ $/\$
104	103	fveq2d 6195	. . . . . . . . . . . . . . . . 17 Word $/\$ lastS $/\$ $/\$ $/\$ ++ ++ ++ ++
105		eqid 2622	. . . . . . . . . . . . . . . . . . . . 21
106	105	2a1i 12	. . . . . . . . . . . . . . . . . . . 20 Word lastS
107	106	imdistani 726	. . . . . . . . . . . . . . . . . . 19 Word $/\$ lastS Word $/\$
108	107	3ad2ant1 1082	. . . . . . . . . . . . . . . . . 18 Word $/\$ lastS $/\$ $/\$ $/\$ Word $/\$
109		simp2l 1087	. . . . . . . . . . . . . . . . . 18 Word $/\$ lastS $/\$ $/\$ $/\$
110		simp2r 1088	. . . . . . . . . . . . . . . . . 18 Word $/\$ lastS $/\$ $/\$ $/\$
111		ccatw2s1p1 13413	. . . . . . . . . . . . . . . . . 18 Word $/\$ $/\$ $/\$ ++ ++
112	108, 109, 110, 111	syl12anc 1324	. . . . . . . . . . . . . . . . 17 Word $/\$ lastS $/\$ $/\$ $/\$ ++ ++
113	104, 112	eqtrd 2656	. . . . . . . . . . . . . . . 16 Word $/\$ lastS $/\$ $/\$ $/\$ ++ ++
114	113	adantr 481	. . . . . . . . . . . . . . 15 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$ ++ ++
115	96, 114	preq12d 4276	. . . . . . . . . . . . . 14 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
116		lsw 13351	. . . . . . . . . . . . . . . . . . . . . . 23 Word lastS
117	116	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word lastS
118		simpl 473	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ Word
119	117, 118	preq12d 4276	. . . . . . . . . . . . . . . . . . . . 21 $/\$ Word lastS
120	119	eleq1d 2686	. . . . . . . . . . . . . . . . . . . 20 $/\$ Word lastS
121	120	biimpd 219	. . . . . . . . . . . . . . . . . . 19 $/\$ Word lastS
122	121	expcom 451	. . . . . . . . . . . . . . . . . 18 Word lastS
123	122	com23 86	. . . . . . . . . . . . . . . . 17 Word lastS
124	123	imp31 448	. . . . . . . . . . . . . . . 16 Word $/\$ lastS $/\$
125	124	3adant2 1080	. . . . . . . . . . . . . . 15 Word $/\$ lastS $/\$ $/\$ $/\$
126	125	adantr 481	. . . . . . . . . . . . . 14 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$
127	115, 126	eqeltrd 2701	. . . . . . . . . . . . 13 Word $/\$ lastS $/\$ $/\$ $/\$ $/\$ $/\$ ++ ++ ++ ++
128	127	exp520 1288	. . . . . . . . . . . 12 Word $/\$ lastS $/\$ ++ ++ ++ ++
129	128	com14 96	. . . . . . . . . . 11 $/\$ Word $/\$ lastS ++ ++ ++ ++
130	129	3ad2ant3 1084	. . . . . . . . . 10 USGraph $/\$ $/\$ $/\$ Word $/\$ lastS ++ ++ ++ ++
131	68, 130	syld 47	. . . . . . . . 9 USGraph $/\$ $/\$ NeighbVtx Word $/\$ lastS ++ ++ ++ ++
132	131	com25 99	. . . . . . . 8 USGraph $/\$ $/\$ Word $/\$ lastS NeighbVtx ++ ++ ++ ++
133	132	com14 96	. . . . . . 7 Word $/\$ lastS USGraph $/\$ $/\$ NeighbVtx ++ ++ ++ ++
134	133	3adant2 1080	. . . . . 6 Word $/\$ ..^ $/\$ lastS USGraph $/\$ $/\$ NeighbVtx ++ ++ ++ ++
135	134	3imp 1256	. . . . 5 Word $/\$ ..^ $/\$ lastS $/\$ $/\$ USGraph $/\$ $/\$ NeighbVtx ++ ++ ++ ++
136	135	impcom 446	. . . 4 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx ++ ++ ++ ++
137	136	imp 445	. . 3 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ++ ++ ++ ++
138	105, 111	mpanl2 717	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ ++ ++
139		ccatw2s1p2 13414	. . . . . . . . . . . . . . . . 17 Word $/\$ $/\$ $/\$ ++ ++
140	105, 139	mpanl2 717	. . . . . . . . . . . . . . . 16 Word $/\$ $/\$ ++ ++
141	138, 140	preq12d 4276	. . . . . . . . . . . . . . 15 Word $/\$ $/\$ ++ ++ ++ ++
142	141	expcom 451	. . . . . . . . . . . . . 14 $/\$ Word ++ ++ ++ ++
143	142	expcom 451	. . . . . . . . . . . . 13 Word ++ ++ ++ ++
144	64, 143	syl6 35	. . . . . . . . . . . 12 USGraph NeighbVtx Word ++ ++ ++ ++
145	144	com24 95	. . . . . . . . . . 11 USGraph Word NeighbVtx ++ ++ ++ ++
146	145	com12 32	. . . . . . . . . 10 Word USGraph NeighbVtx ++ ++ ++ ++
147	146	impd 447	. . . . . . . . 9 Word USGraph $/\$ NeighbVtx ++ ++ ++ ++
148	147	3ad2ant1 1082	. . . . . . . 8 Word $/\$ ..^ $/\$ lastS USGraph $/\$ NeighbVtx ++ ++ ++ ++
149	148	3ad2ant1 1082	. . . . . . 7 Word $/\$ ..^ $/\$ lastS $/\$ $/\$ USGraph $/\$ NeighbVtx ++ ++ ++ ++
150	149	com12 32	. . . . . 6 USGraph $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx ++ ++ ++ ++
151	150	3adant3 1081	. . . . 5 USGraph $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx ++ ++ ++ ++
152	151	imp31 448	. . . 4 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ++ ++ ++ ++
153		numclwwlkovf2exlem2.e	. . . . . . . . 9 Edg
154	153	nbusgreledg 26249	. . . . . . . 8 USGraph NeighbVtx
155		prcom 4267	. . . . . . . . . 10
156	155	eleq1i 2692	. . . . . . . . 9
157	156	biimpi 206	. . . . . . . 8
158	154, 157	syl6bi 243	. . . . . . 7 USGraph NeighbVtx
159	158	3ad2ant1 1082	. . . . . 6 USGraph $/\$ $/\$ NeighbVtx
160	159	adantr 481	. . . . 5 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ NeighbVtx
161	160	imp 445	. . . 4 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx
162	152, 161	eqeltrd 2701	. . 3 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ++ ++ ++ ++
163		ovex 6678	. . . 4
164		fvex 6201	. . . 4
165		fveq2 6191	. . . . . 6 ++ ++ ++ ++
166		oveq1 6657	. . . . . . 7
167	166	fveq2d 6195	. . . . . 6 ++ ++ ++ ++
168	165, 167	preq12d 4276	. . . . 5 ++ ++ ++ ++ ++ ++ ++ ++
169	168	eleq1d 2686	. . . 4 ++ ++ ++ ++ ++ ++ ++ ++
170		fveq2 6191	. . . . . 6 ++ ++ ++ ++
171		oveq1 6657	. . . . . . 7
172	171	fveq2d 6195	. . . . . 6 ++ ++ ++ ++
173	170, 172	preq12d 4276	. . . . 5 ++ ++ ++ ++ ++ ++ ++ ++
174	173	eleq1d 2686	. . . 4 ++ ++ ++ ++ ++ ++ ++ ++
175	163, 164, 169, 174	ralpr 4238	. . 3 ++ ++ ++ ++ ++ ++ ++ ++ $/\$ ++ ++ ++ ++
176	137, 162, 175	sylanbrc 698	. 2 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ++ ++ ++ ++
177		ralunb 3794	. 2 ..^ ++ ++ ++ ++ ..^ ++ ++ ++ ++ $/\$ ++ ++ ++ ++
178	63, 176, 177	sylanbrc 698	1 USGraph $/\$ $/\$ $/\$ Word $/\$ ..^ $/\$ lastS $/\$ $/\$ $/\$ NeighbVtx ..^ ++ ++ ++ ++

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wral 2912

cun 3572

cpr 4179 class class class wbr 4653

cfv 5888 (class class class)co 6650

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

clt 10074

cmin 10266

cn 11020

c2 11070

c3 11071

cn0 11292

cuz 11687 ..^cfzo 12465

chash 13117 Word cword 13291 lastS clsw 13292 ++ cconcat 13293

cs1 13294 Vtxcvtx 25874 Edgcedg 25939 USGraph cusgr 26044 NeighbVtx cnbgr 26224

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 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-fal 1489 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-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-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-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-3 11080 df-n0 11293 df-xnn0 11364 df-z 11378 df-uz 11688 df-fz 12327 df-fzo 12466 df-hash 13118 df-word 13299 df-lsw 13300 df-concat 13301 df-s1 13302 df-edg 25940 df-upgr 25977 df-umgr 25978 df-usgr 26046 df-nbgr 26228

This theorem is referenced by: numclwwlkovf2ex 27219

W3C validator