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 30596

Description: Lemma 2 for clwlkisclwwlklem2 30597. (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 23434	. . . . . . . . . . . . . 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 11705	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$
7		lencl 12368	. . . . . . . . . . . . . . . . . . . . . . . 24 Word
8		simpl 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
9	8	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
10		elnn0z 10771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
11		0re 9498	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
12	11	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
13		zre 10762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
14	13	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
15		nn0re 10700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
16		2re 10503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
17	16	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
18	15, 17	resubcld 9888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
19	18	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
20		lelttr 9577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
21	12, 14, 19, 20	syl3anc 1219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
22		nn0z 10781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
23		2z 10790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
24	23	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
25	22, 24	zsubcld 10864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
26	25	anim1i 568	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
27		elnnz 10768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
28	26, 27	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
29		nn0cn 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
30		cnm1cn 30316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
31	29, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
32	31	subid1d 9820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
33	32	oveq1d 6216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
34		ax-1cn 9452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
35	34	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
36	29, 35, 35	subsub4d 9862	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
37		1p1e2 10547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
38	37	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
39	38	oveq2d 6217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
40	36, 39	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
41	33, 40	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
42	41	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
57	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
58	57	oveq2d 6217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
59	32	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
60	59	oveq1d 6216	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
61	58, 36, 60	3eqtr2d 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
62	61	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
63	62	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
64	63	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
65	64	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
66	65	impcom 430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
67		elfzo0 11705	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5800	. . . . . . . . . . . . . . . . . . . . 21
84		oveq1 6208	. . . . . . . . . . . . . . . . . . . . . 22
85	84	fveq2d 5804	. . . . . . . . . . . . . . . . . . . . 21
86	83, 85	preq12d 4071	. . . . . . . . . . . . . . . . . . . 20
87	86	eleq1d 2523	. . . . . . . . . . . . . . . . . . 19
88	87	adantl 466	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ $/\$
89	82, 88	rspcdv 3182	. . . . . . . . . . . . . . . . 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 6099	. . . . . . . . . . 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 10781	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
103		peano2zm 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
104	22, 103	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
105	102, 104	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
106		zltlem1 10809	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
107	105, 106	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
108	40	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
109	108	breq2d 4413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
110	109	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
111	107, 110	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
112	111	impancom 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
113	112	imp 429	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
114		nn0re 10700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
115	114	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
116	115, 18	anim12i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
117		lenlt 9565	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5804	. . . . . . . . . . . . . . . . . . . . . 22 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
136	135	preq1d 4069	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
137	136	eleq1d 2523	. . . . . . . . . . . . . . . . . . . 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 6099	. . . . . . . . . . 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 3939	. . . . . . 7 $/\$ $\/$ $/\$
153	151, 152	sylibr 212	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
154		clwlkisclwwlklem2.f	. . . . . 6 ..^
155	153, 154	fmptd 5977	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
156		iswrdi 12358	. . . . 5 ..^ Word
157	155, 156	syl 16	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word
158		wrdf 12359	. . . . . . . 8 Word ..^
159	158	adantr 465	. . . . . . 7 Word $/\$ ..^
160	154	clwlkisclwwlklem2a2 30591	. . . . . . . . 9 Word $/\$
161		fzoval 11672	. . . . . . . . . . 11 ..^
162	7, 22, 161	3syl 20	. . . . . . . . . 10 Word ..^
163		oveq2 6209	. . . . . . . . . . 11
164	163	eqcoms 2466	. . . . . . . . . 10
165	162, 164	sylan9eq 2515	. . . . . . . . 9 Word $/\$ ..^
166	160, 165	syldan 470	. . . . . . . 8 Word $/\$ ..^
167	166	feq2d 5656	. . . . . . 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 30590	. . . . . 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 30595	. . . . . . . . . 10 USGrph $/\$ Word $/\$ lastS $/\$ ..^
176	175	impl 620	. . . . . . . . 9 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^
177	176	ralimdva 2832	. . . . . . . 8 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
178		oveq2 6209	. . . . . . . . . 10 ..^ ..^
179	178	raleqdv 3029	. . . . . . . . 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 30592	. . . . . . . . . 10 Word $/\$ lastS
187	186	3adant1 1006	. . . . . . . . 9 USGrph $/\$ Word $/\$ lastS
188	187	eqcomd 2462	. . . . . . . 8 USGrph $/\$ Word $/\$ lastS
189	188	eqeq2d 2468	. . . . . . 7 USGrph $/\$ Word $/\$ lastS
190	189	biimpcd 224	. . . . . 6 lastS USGrph $/\$ Word $/\$
191	190	eqcoms 2466	. . . . 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 1370

wcel 1758

wral 2799

cif 3900

cpr 3988 class class class wbr 4401

cmpt 4459

ccnv 4948

cdm 4949

crn 4950

wf 5523

wf1o 5526

cfv 5527 (class class class)co 6201

cc 9392

cr 9393

cc0 9394

c1 9395

caddc 9397

clt 9530

cle 9531

cmin 9707

cn 10434

c2 10483

cn0 10691

cz 10758

cfz 11555 ..^cfzo 11666

chash 12221 Word cword 12340 lastS clsw 12341 USGrph cusg 23417

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4512 ax-sep 4522 ax-nul 4530 ax-pow 4579 ax-pr 4640 ax-un 6483 ax-cnex 9450 ax-resscn 9451 ax-1cn 9452 ax-icn 9453 ax-addcl 9454 ax-addrcl 9455 ax-mulcl 9456 ax-mulrcl 9457 ax-mulcom 9458 ax-addass 9459 ax-mulass 9460 ax-distr 9461 ax-i2m1 9462 ax-1ne0 9463 ax-1rid 9464 ax-rnegex 9465 ax-rrecex 9466 ax-cnre 9467 ax-pre-lttri 9468 ax-pre-lttrn 9469 ax-pre-ltadd 9470 ax-pre-mulgt0 9471

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-nel 2651 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-pss 3453 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-tp 3991 df-op 3993 df-uni 4201 df-int 4238 df-iun 4282 df-br 4402 df-opab 4460 df-mpt 4461 df-tr 4495 df-eprel 4741 df-id 4745 df-po 4750 df-so 4751 df-fr 4788 df-we 4790 df-ord 4831 df-on 4832 df-lim 4833 df-suc 4834 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-res 4961 df-ima 4962 df-iota 5490 df-fun 5529 df-fn 5530 df-f 5531 df-f1 5532 df-fo 5533 df-f1o 5534 df-fv 5535 df-riota 6162 df-ov 6204 df-oprab 6205 df-mpt2 6206 df-om 6588 df-1st 6688 df-2nd 6689 df-recs 6943 df-rdg 6977 df-1o 7031 df-oadd 7035 df-er 7212 df-en 7422 df-dom 7423 df-sdom 7424 df-fin 7425 df-card 8221 df-pnf 9532 df-mnf 9533 df-xr 9534 df-ltxr 9535 df-le 9536 df-sub 9709 df-neg 9710 df-nn 10435 df-2 10492 df-n0 10692 df-z 10759 df-uz 10974 df-fz 11556 df-fzo 11667 df-hash 12222 df-word 12348 df-lsw 12349 df-usgra 23419

This theorem is referenced by: clwlkisclwwlklem2 30597

W3C validator