clwlkisclwwlklem2a - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > clwlkisclwwlklem2a		Structured version Unicode version

Theorem clwlkisclwwlklem2a 30400

Description: Lemma 2 for clwlkisclwwlklem2 30401. (Contributed by Alexander van der Vekens, 22-Jun-2018.)

**Hypothesis**
Ref	Expression
clwlkisclwwlklem2.f	..^

**Assertion**
Ref	Expression
clwlkisclwwlklem2a	USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$

Distinct variable groups:

Allowed substitution hint:

(

)

**Proof of Theorem clwlkisclwwlklem2a**
Step	Hyp	Ref	Expression
1		simpl 457	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
2		usgraf1o 23232	. . . . . . . . . . . . . 14 USGrph
3	2	3ad2ant1 1009	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$
4	3	adantr 465	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
5	4	ad2antrl 727	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
6		elfzo0 11579	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$
7		lencl 12241	. . . . . . . . . . . . . . . . . . . . . . . 24 Word
8		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
9	8	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
10		elnn0z 10651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
11		0re 9378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
12	11	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
13		zre 10642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
14	13	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
15		nn0re 10580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
16		2re 10383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
17	16	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
18	15, 17	resubcld 9768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
19	18	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
20		lelttr 9457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
21	12, 14, 19, 20	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
22		nn0z 10661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
23		2z 10670	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
24	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
25	22, 24	zsubcld 10744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
26	25	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
27		elnnz 10648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
28	26, 27	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
29		nn0cn 10581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
30		cnm1cn 30120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
31	29, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
32	31	subid1d 9700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
33	32	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
34		ax-1cn 9332	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
36	29, 35, 35	subsub4d 9742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
37		1p1e2 10427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
39	38	oveq2d 6102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
40	36, 39	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
41	33, 40	eqtrd 2470	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
42	41	eleq1d 2504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
43	42	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
44	28, 43	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
45	44	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
46	45	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
47	21, 46	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
48	47	exp4b 607	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
49	48	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
50	49	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
51	10, 50	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
52	51	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
53	52	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
54	53	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
55	54	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
56		df-2 10372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
58	57	oveq2d 6102	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
59	32	eqcomd 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
60	59	oveq1d 6101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
61	58, 36, 60	3eqtr2d 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
62	61	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
63	62	breq2d 4299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
64	63	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
65	64	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
66	65	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
67		elfzo0 11579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $/\$ $/\$
68	9, 55, 66, 67	syl3anbrc 1172	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ ..^
69	68	exp32 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^
70	69	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^
71	70	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^
72	71	ex 434	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
73	72	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
74	73	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
75	74	3adant2 1007	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
76	75	com14 88	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
77	7, 76	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ ..^
78	77	imp 429	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ $/\$ ..^
79	78	3adant1 1006	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
80	6, 79	syl7bi 230	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ Word $/\$ ..^ ..^
81	80	com13 80	. . . . . . . . . . . . . . . . . . 19 ..^ USGrph $/\$ Word $/\$ ..^
82	81	imp31 432	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ ..^
83		fveq2 5686	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6093	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	preq12d 3957	. . . . . . . . . . . . . . . . . . . 20
87	86	eleq1d 2504	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 466	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ $/\$
89	82, 88	rspcdv 3071	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ ..^
90	89	ex 434	. . . . . . . . . . . . . . . 16 ..^ $/\$ USGrph $/\$ Word $/\$ ..^
91	90	com13 80	. . . . . . . . . . . . . . 15 ..^ USGrph $/\$ Word $/\$ ..^ $/\$
92	91	ad2antrl 727	. . . . . . . . . . . . . 14 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$ ..^ $/\$
93	92	impcom 430	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^ $/\$
94	93	expdimp 437	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
95	94	impcom 430	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
96		f1ocnvdm 5984	. . . . . . . . . . 11 $/\$
97	5, 95, 96	syl2anc 661	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
98	1, 97	jca 532	. . . . . . . . 9 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$
99	98	orcd 392	. . . . . . . 8 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
100		simpl 457	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
101	4	ad2antrl 727	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
102		nn0z 10661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
103		peano2zm 10680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
104	22, 103	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
105	102, 104	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
106		zltlem1 10689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
107	105, 106	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
108	40	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
109	108	breq2d 4299	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
110	109	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
111	107, 110	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
112	111	impancom 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
113	112	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
114		nn0re 10580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
115	114	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
116	115, 18	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
117		lenlt 9445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
118	116, 117	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
119	113, 118	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
120	119	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
121	116	ancomd 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
122	121	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
123		lttri3 9450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
124	122, 123	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
125	120, 124	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
126	125	exp31 604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	126	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
128	127	3adant2 1007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
129	6, 128	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
130	129	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^
131	130	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
132	7, 131	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ ..^
133	132	3ad2ant2 1010	. . . . . . . . . . . . . . . . . . . . . . . 24 USGrph $/\$ Word $/\$ $/\$ ..^
134	133	imp 429	. . . . . . . . . . . . . . . . . . . . . . 23 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
135	134	fveq2d 5690	. . . . . . . . . . . . . . . . . . . . . 22 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
136	135	preq1d 3955	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
137	136	eleq1d 2504	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
138	137	biimpd 207	. . . . . . . . . . . . . . . . . . 19 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
139	138	exp32 605	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ Word $/\$ ..^
140	139	com12 31	. . . . . . . . . . . . . . . . 17 USGrph $/\$ Word $/\$ ..^
141	140	com14 88	. . . . . . . . . . . . . . . 16 USGrph $/\$ Word $/\$ ..^
142	141	adantl 466	. . . . . . . . . . . . . . 15 ..^ $/\$ USGrph $/\$ Word $/\$ ..^
143	142	adantl 466	. . . . . . . . . . . . . 14 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$ ..^
144	143	com12 31	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ ..^
145	144	imp31 432	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
146	145	impcom 430	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
147		f1ocnvdm 5984	. . . . . . . . . . 11 $/\$
148	101, 146, 147	syl2anc 661	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
149	100, 148	jca 532	. . . . . . . . 9 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$
150	149	olcd 393	. . . . . . . 8 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
151	99, 150	pm2.61ian 788	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
152		ifel 3825	. . . . . . 7 $/\$ $\/$ $/\$
153	151, 152	sylibr 212	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
154		clwlkisclwwlklem2.f	. . . . . 6 ..^
155	153, 154	fmptd 5862	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
156		iswrdi 12231	. . . . 5 ..^ Word
157	155, 156	syl 16	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word
158		wrdf 12232	. . . . . . . 8 Word ..^
159	158	adantr 465	. . . . . . 7 Word $/\$ ..^
160	154	clwlkisclwwlklem2a2 30395	. . . . . . . . 9 Word $/\$
161		fzoval 11546	. . . . . . . . . . 11 ..^
162	7, 22, 161	3syl 20	. . . . . . . . . 10 Word ..^
163		oveq2 6094	. . . . . . . . . . 11
164	163	eqcoms 2441	. . . . . . . . . 10
165	162, 164	sylan9eq 2490	. . . . . . . . 9 Word $/\$ ..^
166	160, 165	syldan 470	. . . . . . . 8 Word $/\$ ..^
167	166	feq2d 5542	. . . . . . 7 Word $/\$ ..^
168	159, 167	mpbid 210	. . . . . 6 Word $/\$
169	168	3adant1 1006	. . . . 5 USGrph $/\$ Word $/\$
170	169	adantr 465	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
171		clwlkisclwwlklem2a1 30394	. . . . . 6 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ ..^
172	171	imp 429	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
173	160	3adant1 1006	. . . . . . . 8 USGrph $/\$ Word $/\$
174	173	adantr 465	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS
175	154	clwlkisclwwlklem2a4 30399	. . . . . . . . . 10 USGrph $/\$ Word $/\$ lastS $/\$ ..^
176	175	impl 620	. . . . . . . . 9 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^
177	176	ralimdva 2789	. . . . . . . 8 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
178		oveq2 6094	. . . . . . . . . 10 ..^ ..^
179	178	raleqdv 2918	. . . . . . . . 9 ..^ ..^
180	179	imbi2d 316	. . . . . . . 8 ..^ ..^ ..^ ..^
181	177, 180	syl5ibr 221	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
182	174, 181	mpcom 36	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
183	182	adantrr 716	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^ ..^
184	172, 183	mpd 15	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
185	157, 170, 184	3jca 1168	. . 3 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^
186	154	clwlkisclwwlklem2a3 30396	. . . . . . . . . 10 Word $/\$ lastS
187	186	3adant1 1006	. . . . . . . . 9 USGrph $/\$ Word $/\$ lastS
188	187	eqcomd 2443	. . . . . . . 8 USGrph $/\$ Word $/\$ lastS
189	188	eqeq2d 2449	. . . . . . 7 USGrph $/\$ Word $/\$ lastS
190	189	biimpcd 224	. . . . . 6 lastS USGrph $/\$ Word $/\$
191	190	eqcoms 2441	. . . . 5 lastS USGrph $/\$ Word $/\$
192	191	adantr 465	. . . 4 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$
193	192	impcom 430	. . 3 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
194	185, 193	jca 532	. 2 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$
195	194	ex 434	1 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756

wral 2710

cif 3786

cpr 3874 class class class wbr 4287

cmpt 4345

ccnv 4834

cdm 4835

crn 4836

wf 5409

wf1o 5412

cfv 5413 (class class class)co 6086

cc 9272

cr 9273

cc0 9274

c1 9275

caddc 9277

clt 9410

cle 9411

cmin 9587

cn 10314

c2 10363

cn0 10571

cz 10638

cfz 11429 ..^cfzo 11540

chash 12095 Word cword 12213 lastS clsw 12214 USGrph cusg 23215

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-cnex 9330 ax-resscn 9331 ax-1cn 9332 ax-icn 9333 ax-addcl 9334 ax-addrcl 9335 ax-mulcl 9336 ax-mulrcl 9337 ax-mulcom 9338 ax-addass 9339 ax-mulass 9340 ax-distr 9341 ax-i2m1 9342 ax-1ne0 9343 ax-1rid 9344 ax-rnegex 9345 ax-rrecex 9346 ax-cnre 9347 ax-pre-lttri 9348 ax-pre-lttrn 9349 ax-pre-ltadd 9350 ax-pre-mulgt0 9351

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-pss 3339 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-tp 3877 df-op 3879 df-uni 4087 df-int 4124 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-tr 4381 df-eprel 4627 df-id 4631 df-po 4636 df-so 4637 df-fr 4674 df-we 4676 df-ord 4717 df-on 4718 df-lim 4719 df-suc 4720 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-om 6472 df-1st 6572 df-2nd 6573 df-recs 6824 df-rdg 6858 df-1o 6912 df-oadd 6916 df-er 7093 df-en 7303 df-dom 7304 df-sdom 7305 df-fin 7306 df-card 8101 df-pnf 9412 df-mnf 9413 df-xr 9414 df-ltxr 9415 df-le 9416 df-sub 9589 df-neg 9590 df-nn 10315 df-2 10372 df-n0 10572 df-z 10639 df-uz 10854 df-fz 11430 df-fzo 11541 df-hash 12096 df-word 12221 df-lsw 12222 df-usgra 23217

This theorem is referenced by: clwlkisclwwlklem2 30401

W3C validator