clwlkisclwwlklem2a - Metamath Proof Explorer

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

Theorem clwlkisclwwlklem2a 24987

Description: Lemma 2 for clwlkisclwwlklem2 24988. (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 455	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
2		usgraf1o 24560	. . . . . . . . . . . . . 14 USGrph
3	2	3ad2ant1 1015	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$
4	3	adantr 463	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
5	4	ad2antrl 725	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
6		elfzo0 11840	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$
7		lencl 12549	. . . . . . . . . . . . . . . . . . . . . . . 24 Word
8		simpl 455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
9	8	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
10		elnn0z 10873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
11		0red 9586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
12		zre 10864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
13	12	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
14		nn0re 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
15		2re 10601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
16	15	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
17	14, 16	resubcld 9983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
18	17	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
19		lelttr 9664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
20	11, 13, 18, 19	syl3anc 1226	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
21		nn0z 10883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
22		2z 10892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
24	21, 23	zsubcld 10970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
25	24	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
26		elnnz 10870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
27	25, 26	sylibr 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
28		nn0cn 10801	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
29		peano2cnm 9876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
30	28, 29	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
31	30	subid1d 9911	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
32	31	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
33		1cnd 9601	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
34	28, 33, 33	subsub4d 9953	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
35		1p1e2 10645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
36	35	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
37	36	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
38	34, 37	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
39	32, 38	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
40	39	eleq1d 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
41	40	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
42	27, 41	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
43	42	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
44	43	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
45	20, 44	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
46	45	exp4b 605	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
47	46	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
48	47	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
49	10, 48	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
50	49	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
51	50	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
52	51	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
53	52	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
54		df-2 10590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
56	55	oveq2d 6286	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
57	31	eqcomd 2462	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
58	57	oveq1d 6285	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
59	56, 34, 58	3eqtr2d 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
60	59	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
61	60	breq2d 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
62	61	biimpcd 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
63	62	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
64	63	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
65		elfzo0 11840	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $/\$ $/\$
66	9, 53, 64, 65	syl3anbrc 1178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ ..^
67	66	exp32 603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^
68	67	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^
69	68	com24 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^
70	69	ex 432	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
71	70	com25 91	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
72	71	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
73	72	3adant2 1013	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
74	73	com14 88	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
75	7, 74	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ ..^
76	75	imp 427	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ $/\$ ..^
77	76	3adant1 1012	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
78	6, 77	syl7bi 230	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ Word $/\$ ..^ ..^
79	78	com13 80	. . . . . . . . . . . . . . . . . . 19 ..^ USGrph $/\$ Word $/\$ ..^
80	79	imp31 430	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ ..^
81		fveq2 5848	. . . . . . . . . . . . . . . . . . . . 21
82		oveq1 6277	. . . . . . . . . . . . . . . . . . . . . 22
83	82	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . 21
84	81, 83	preq12d 4103	. . . . . . . . . . . . . . . . . . . 20
85	84	eleq1d 2523	. . . . . . . . . . . . . . . . . . 19
86	85	adantl 464	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ $/\$
87	80, 86	rspcdv 3210	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ ..^
88	87	ex 432	. . . . . . . . . . . . . . . 16 ..^ $/\$ USGrph $/\$ Word $/\$ ..^
89	88	com13 80	. . . . . . . . . . . . . . 15 ..^ USGrph $/\$ Word $/\$ ..^ $/\$
90	89	ad2antrl 725	. . . . . . . . . . . . . 14 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$ ..^ $/\$
91	90	impcom 428	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^ $/\$
92	91	expdimp 435	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
93	92	impcom 428	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
94		f1ocnvdm 6163	. . . . . . . . . . 11 $/\$
95	5, 93, 94	syl2anc 659	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
96	1, 95	jca 530	. . . . . . . . 9 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$
97	96	orcd 390	. . . . . . . 8 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
98		simpl 455	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
99	4	ad2antrl 725	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
100		nn0z 10883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		peano2zm 10903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
102	21, 101	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
103	100, 102	anim12i 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
104		zltlem1 10912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
105	103, 104	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
106	38	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
107	106	breq2d 4451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
108	107	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
109	105, 108	sylbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
110	109	impancom 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
111	110	imp 427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
112		nn0re 10800	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
113	112	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
114	113, 17	anim12i 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
115		lenlt 9652	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
116	114, 115	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
117	111, 116	mpbid 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
118	117	anim1i 566	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
119	114	ancomd 449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
120	119	adantr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
121		lttri3 9657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
122	120, 121	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
123	118, 122	mpbird 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
124	123	exp31 602	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
125	124	com23 78	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
126	125	3adant2 1013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
127	6, 126	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
128	127	impcom 428	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^
129	128	com12 31	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
130	7, 129	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ ..^
131	130	3ad2ant2 1016	. . . . . . . . . . . . . . . . . . . . . . . 24 USGrph $/\$ Word $/\$ $/\$ ..^
132	131	imp 427	. . . . . . . . . . . . . . . . . . . . . . 23 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
133	132	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . 22 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
134	133	preq1d 4101	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
135	134	eleq1d 2523	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
136	135	biimpd 207	. . . . . . . . . . . . . . . . . . 19 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
137	136	exp32 603	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ Word $/\$ ..^
138	137	com12 31	. . . . . . . . . . . . . . . . 17 USGrph $/\$ Word $/\$ ..^
139	138	com14 88	. . . . . . . . . . . . . . . 16 USGrph $/\$ Word $/\$ ..^
140	139	adantl 464	. . . . . . . . . . . . . . 15 ..^ $/\$ USGrph $/\$ Word $/\$ ..^
141	140	adantl 464	. . . . . . . . . . . . . 14 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$ ..^
142	141	com12 31	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ ..^
143	142	imp31 430	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
144	143	impcom 428	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
145		f1ocnvdm 6163	. . . . . . . . . . 11 $/\$
146	99, 144, 145	syl2anc 659	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
147	98, 146	jca 530	. . . . . . . . 9 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$
148	147	olcd 391	. . . . . . . 8 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
149	97, 148	pm2.61ian 788	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
150		ifel 3970	. . . . . . 7 $/\$ $\/$ $/\$
151	149, 150	sylibr 212	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
152		clwlkisclwwlklem2.f	. . . . . 6 ..^
153	151, 152	fmptd 6031	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
154		iswrdi 12537	. . . . 5 ..^ Word
155	153, 154	syl 16	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word
156		wrdf 12538	. . . . . . . 8 Word ..^
157	156	adantr 463	. . . . . . 7 Word $/\$ ..^
158	152	clwlkisclwwlklem2a2 24982	. . . . . . . . 9 Word $/\$
159		fzoval 11805	. . . . . . . . . . 11 ..^
160	7, 21, 159	3syl 20	. . . . . . . . . 10 Word ..^
161		oveq2 6278	. . . . . . . . . . 11
162	161	eqcoms 2466	. . . . . . . . . 10
163	160, 162	sylan9eq 2515	. . . . . . . . 9 Word $/\$ ..^
164	158, 163	syldan 468	. . . . . . . 8 Word $/\$ ..^
165	164	feq2d 5700	. . . . . . 7 Word $/\$ ..^
166	157, 165	mpbid 210	. . . . . 6 Word $/\$
167	166	3adant1 1012	. . . . 5 USGrph $/\$ Word $/\$
168	167	adantr 463	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
169		clwlkisclwwlklem2a1 24981	. . . . . 6 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ ..^
170	169	imp 427	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
171	158	3adant1 1012	. . . . . . . 8 USGrph $/\$ Word $/\$
172	171	adantr 463	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS
173	152	clwlkisclwwlklem2a4 24986	. . . . . . . . . 10 USGrph $/\$ Word $/\$ lastS $/\$ ..^
174	173	impl 618	. . . . . . . . 9 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^
175	174	ralimdva 2862	. . . . . . . 8 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
176		oveq2 6278	. . . . . . . . . 10 ..^ ..^
177	176	raleqdv 3057	. . . . . . . . 9 ..^ ..^
178	177	imbi2d 314	. . . . . . . 8 ..^ ..^ ..^ ..^
179	175, 178	syl5ibr 221	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
180	172, 179	mpcom 36	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
181	180	adantrr 714	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^ ..^
182	170, 181	mpd 15	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
183	155, 168, 182	3jca 1174	. . 3 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^
184	152	clwlkisclwwlklem2a3 24983	. . . . . . . . . 10 Word $/\$ lastS
185	184	3adant1 1012	. . . . . . . . 9 USGrph $/\$ Word $/\$ lastS
186	185	eqcomd 2462	. . . . . . . 8 USGrph $/\$ Word $/\$ lastS
187	186	eqeq2d 2468	. . . . . . 7 USGrph $/\$ Word $/\$ lastS
188	187	biimpcd 224	. . . . . 6 lastS USGrph $/\$ Word $/\$
189	188	eqcoms 2466	. . . . 5 lastS USGrph $/\$ Word $/\$
190	189	adantr 463	. . . 4 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$
191	190	impcom 428	. . 3 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
192	183, 191	jca 530	. 2 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$
193	192	ex 432	1 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $/\$ w3a 971

wceq 1398

wcel 1823

wral 2804

cif 3929

cpr 4018 class class class wbr 4439

cmpt 4497

ccnv 4987

cdm 4988

crn 4989

wf 5566

wf1o 5569

cfv 5570 (class class class)co 6270

cc 9479

cr 9480

cc0 9481

c1 9482

caddc 9484

clt 9617

cle 9618

cmin 9796

cn 10531

c2 10581

cn0 10791

cz 10860

cfz 11675 ..^cfzo 11799

chash 12387 Word cword 12518 lastS clsw 12519 USGrph cusg 24532

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rmo 2812 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-int 4272 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-1o 7122 df-oadd 7126 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-fin 7513 df-card 8311 df-cda 8539 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-nn 10532 df-2 10590 df-n0 10792 df-z 10861 df-uz 11083 df-fz 11676 df-fzo 11800 df-hash 12388 df-word 12526 df-lsw 12527 df-usgra 24535

This theorem is referenced by: clwlkisclwwlklem2 24988

W3C validator