clwlkisclwwlklem2a - Metamath Proof Explorer

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

Theorem clwlkisclwwlklem2a 25569

Description: Lemma 2 for clwlkisclwwlklem2 25570. (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 463	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
2		usgraf1o 25141	. . . . . . . . . . . . . 14 USGrph
3	2	3ad2ant1 1035	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$
4	3	adantr 471	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
5	4	ad2antrl 739	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
6		elfzo0 11993	. . . . . . . . . . . . . . . . . . . . 21 ..^ $/\$ $/\$
7		lencl 12728	. . . . . . . . . . . . . . . . . . . . . . . 24 Word
8		simpl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
9	8	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
10		elnn0z 10984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
11		0red 9675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
12		zre 10975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
13	12	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
14		nn0re 10912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
15		2re 10712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
16	15	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
17	14, 16	resubcld 10080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
18	17	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
19		lelttr 9755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
20	11, 13, 18, 19	syl3anc 1276	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
21		nn0z 10994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
22		2z 11003	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
23	22	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
24	21, 23	zsubcld 11079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
25	24	anim1i 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
26		elnnz 10981	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
27	25, 26	sylibr 217	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
28		nn0cn 10913	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
29		peano2cnm 9971	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
30	28, 29	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
31	30	subid1d 10006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
32	31	oveq1d 6335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
33		1cnd 9690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
34	28, 33, 33	subsub4d 10048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
35		1p1e2 10756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
36	35	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
37	36	oveq2d 6336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
38	34, 37	eqtrd 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
39	32, 38	eqtrd 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
40	39	eleq1d 2524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
41	40	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
42	27, 41	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
43	42	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
44	43	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
45	20, 44	syld 45	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
46	45	exp4b 616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
47	46	com23 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
48	47	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
49	10, 48	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
50	49	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
51	50	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
52	51	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
53	52	impcom 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
54		df-2 10701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
55	54	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
56	55	oveq2d 6336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
57	31	eqcomd 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
58	57	oveq1d 6335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
59	56, 34, 58	3eqtr2d 2502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
60	59	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
61	60	breq2d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
62	61	biimpcd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
63	62	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
64	63	impcom 436	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$
65		elfzo0 11993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ..^ $/\$ $/\$
66	9, 53, 64, 65	syl3anbrc 1198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ ..^
67	66	exp32 614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ ..^
68	67	a1d 26	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ ..^
69	68	com24 90	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ ..^
70	69	ex 440	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
71	70	com25 94	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ..^
72	71	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
73	72	3adant2 1033	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ ..^
74	73	com14 91	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ ..^
75	7, 74	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 Word $/\$ $/\$ ..^
76	75	imp 435	. . . . . . . . . . . . . . . . . . . . . 22 Word $/\$ $/\$ $/\$ ..^
77	76	3adant1 1032	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
78	6, 77	syl7bi 238	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ Word $/\$ ..^ ..^
79	78	com13 83	. . . . . . . . . . . . . . . . . . 19 ..^ USGrph $/\$ Word $/\$ ..^
80	79	imp31 438	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ ..^
81		fveq2 5892	. . . . . . . . . . . . . . . . . . . . 21
82		oveq1 6327	. . . . . . . . . . . . . . . . . . . . . 22
83	82	fveq2d 5896	. . . . . . . . . . . . . . . . . . . . 21
84	81, 83	preq12d 4072	. . . . . . . . . . . . . . . . . . . 20
85	84	eleq1d 2524	. . . . . . . . . . . . . . . . . . 19
86	85	adantl 472	. . . . . . . . . . . . . . . . . 18 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ $/\$
87	80, 86	rspcdv 3165	. . . . . . . . . . . . . . . . 17 ..^ $/\$ $/\$ USGrph $/\$ Word $/\$ ..^
88	87	ex 440	. . . . . . . . . . . . . . . 16 ..^ $/\$ USGrph $/\$ Word $/\$ ..^
89	88	com13 83	. . . . . . . . . . . . . . 15 ..^ USGrph $/\$ Word $/\$ ..^ $/\$
90	89	ad2antrl 739	. . . . . . . . . . . . . 14 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$ ..^ $/\$
91	90	impcom 436	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^ $/\$
92	91	expdimp 443	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
93	92	impcom 436	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
94		f1ocnvdm 6213	. . . . . . . . . . 11 $/\$
95	5, 93, 94	syl2anc 671	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
96	1, 95	jca 539	. . . . . . . . 9 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$
97	96	orcd 398	. . . . . . . 8 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
98		simpl 463	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
99	4	ad2antrl 739	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
100		nn0z 10994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		peano2zm 11014	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
102	21, 101	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
103	100, 102	anim12i 574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
104		zltlem1 11023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
105	103, 104	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
106	38	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
107	106	breq2d 4430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
108	107	biimpd 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
109	105, 108	sylbid 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
110	109	impancom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
111	110	imp 435	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
112		nn0re 10912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
113	112	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
114	113, 17	anim12i 574	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
115		lenlt 9743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
116	114, 115	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
117	111, 116	mpbid 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
118	117	anim1i 576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
119	114	ancomd 457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
120	119	adantr 471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
121		lttri3 9748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
122	120, 121	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$
123	118, 122	mpbird 240	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$
124	123	exp31 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
125	124	com23 81	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
126	125	3adant2 1033	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
127	6, 126	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ..^
128	127	impcom 436	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ ..^
129	128	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ ..^
130	7, 129	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 Word $/\$ ..^
131	130	3ad2ant2 1036	. . . . . . . . . . . . . . . . . . . . . . . 24 USGrph $/\$ Word $/\$ $/\$ ..^
132	131	imp 435	. . . . . . . . . . . . . . . . . . . . . . 23 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
133	132	fveq2d 5896	. . . . . . . . . . . . . . . . . . . . . 22 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
134	133	preq1d 4070	. . . . . . . . . . . . . . . . . . . . 21 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
135	134	eleq1d 2524	. . . . . . . . . . . . . . . . . . . 20 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
136	135	biimpd 212	. . . . . . . . . . . . . . . . . . 19 USGrph $/\$ Word $/\$ $/\$ $/\$ ..^
137	136	exp32 614	. . . . . . . . . . . . . . . . . 18 USGrph $/\$ Word $/\$ ..^
138	137	com12 32	. . . . . . . . . . . . . . . . 17 USGrph $/\$ Word $/\$ ..^
139	138	com14 91	. . . . . . . . . . . . . . . 16 USGrph $/\$ Word $/\$ ..^
140	139	adantl 472	. . . . . . . . . . . . . . 15 ..^ $/\$ USGrph $/\$ Word $/\$ ..^
141	140	adantl 472	. . . . . . . . . . . . . 14 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$ ..^
142	141	com12 32	. . . . . . . . . . . . 13 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ ..^
143	142	imp31 438	. . . . . . . . . . . 12 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
144	143	impcom 436	. . . . . . . . . . 11 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
145		f1ocnvdm 6213	. . . . . . . . . . 11 $/\$
146	99, 144, 145	syl2anc 671	. . . . . . . . . 10 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
147	98, 146	jca 539	. . . . . . . . 9 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$
148	147	olcd 399	. . . . . . . 8 $/\$ USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
149	97, 148	pm2.61ian 804	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^ $/\$ $\/$ $/\$
150		ifel 3934	. . . . . . 7 $/\$ $\/$ $/\$
151	149, 150	sylibr 217	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ $/\$ ..^
152		clwlkisclwwlklem2.f	. . . . . 6 ..^
153	151, 152	fmptd 6074	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
154		iswrdi 12714	. . . . 5 ..^ Word
155	153, 154	syl 17	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word
156		wrdf 12715	. . . . . . . 8 Word ..^
157	156	adantr 471	. . . . . . 7 Word $/\$ ..^
158	152	clwlkisclwwlklem2a2 25564	. . . . . . . . 9 Word $/\$
159		fzoval 11958	. . . . . . . . . . 11 ..^
160	7, 21, 159	3syl 18	. . . . . . . . . 10 Word ..^
161		oveq2 6328	. . . . . . . . . . 11
162	161	eqcoms 2470	. . . . . . . . . 10
163	160, 162	sylan9eq 2516	. . . . . . . . 9 Word $/\$ ..^
164	158, 163	syldan 477	. . . . . . . 8 Word $/\$ ..^
165	164	feq2d 5741	. . . . . . 7 Word $/\$ ..^
166	157, 165	mpbid 215	. . . . . 6 Word $/\$
167	166	3adant1 1032	. . . . 5 USGrph $/\$ Word $/\$
168	167	adantr 471	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
169		clwlkisclwwlklem2a1 25563	. . . . . 6 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ ..^
170	169	imp 435	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
171	158	3adant1 1032	. . . . . . . 8 USGrph $/\$ Word $/\$
172	171	adantr 471	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS
173	152	clwlkisclwwlklem2a4 25568	. . . . . . . . . 10 USGrph $/\$ Word $/\$ lastS $/\$ ..^
174	173	impl 630	. . . . . . . . 9 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^
175	174	ralimdva 2808	. . . . . . . 8 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
176		oveq2 6328	. . . . . . . . . 10 ..^ ..^
177	176	raleqdv 3005	. . . . . . . . 9 ..^ ..^
178	177	imbi2d 322	. . . . . . . 8 ..^ ..^ ..^ ..^
179	175, 178	syl5ibr 229	. . . . . . 7 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
180	172, 179	mpcom 37	. . . . . 6 USGrph $/\$ Word $/\$ $/\$ lastS ..^ ..^
181	180	adantrr 728	. . . . 5 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^ ..^
182	170, 181	mpd 15	. . . 4 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ ..^
183	155, 168, 182	3jca 1194	. . 3 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^
184	152	clwlkisclwwlklem2a3 25565	. . . . . . . . . 10 Word $/\$ lastS
185	184	3adant1 1032	. . . . . . . . 9 USGrph $/\$ Word $/\$ lastS
186	185	eqcomd 2468	. . . . . . . 8 USGrph $/\$ Word $/\$ lastS
187	186	eqeq2d 2472	. . . . . . 7 USGrph $/\$ Word $/\$ lastS
188	187	biimpcd 232	. . . . . 6 lastS USGrph $/\$ Word $/\$
189	188	eqcoms 2470	. . . . 5 lastS USGrph $/\$ Word $/\$
190	189	adantr 471	. . . 4 lastS $/\$ ..^ $/\$ USGrph $/\$ Word $/\$
191	190	impcom 436	. . 3 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$
192	183, 191	jca 539	. 2 USGrph $/\$ Word $/\$ $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$
193	192	ex 440	1 USGrph $/\$ Word $/\$ lastS $/\$ ..^ $/\$ Word $/\$ $/\$ ..^ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $\/$ wo 374 $/\$ wa 375 $/\$ w3a 991

wceq 1455

wcel 1898

wral 2749

cif 3893

cpr 3982 class class class wbr 4418

cmpt 4477

ccnv 4855

cdm 4856

crn 4857

wf 5601

wf1o 5604

cfv 5605 (class class class)co 6320

cc 9568

cr 9569

cc0 9570

c1 9571

caddc 9573

clt 9706

cle 9707

cmin 9891

cn 10642

c2 10692

cn0 10903

cz 10971

cfz 11819 ..^cfzo 11952

chash 12553 Word cword 12695 lastS clsw 12696 USGrph cusg 25113

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4531 ax-sep 4541 ax-nul 4550 ax-pow 4598 ax-pr 4656 ax-un 6615 ax-cnex 9626 ax-resscn 9627 ax-1cn 9628 ax-icn 9629 ax-addcl 9630 ax-addrcl 9631 ax-mulcl 9632 ax-mulrcl 9633 ax-mulcom 9634 ax-addass 9635 ax-mulass 9636 ax-distr 9637 ax-i2m1 9638 ax-1ne0 9639 ax-1rid 9640 ax-rnegex 9641 ax-rrecex 9642 ax-cnre 9643 ax-pre-lttri 9644 ax-pre-lttrn 9645 ax-pre-ltadd 9646 ax-pre-mulgt0 9647

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-br 4419 df-opab 4478 df-mpt 4479 df-tr 4514 df-eprel 4767 df-id 4771 df-po 4777 df-so 4778 df-fr 4815 df-we 4817 df-xp 4862 df-rel 4863 df-cnv 4864 df-co 4865 df-dm 4866 df-rn 4867 df-res 4868 df-ima 4869 df-pred 5403 df-ord 5449 df-on 5450 df-lim 5451 df-suc 5452 df-iota 5569 df-fun 5607 df-fn 5608 df-f 5609 df-f1 5610 df-fo 5611 df-f1o 5612 df-fv 5613 df-riota 6282 df-ov 6323 df-oprab 6324 df-mpt2 6325 df-om 6725 df-1st 6825 df-2nd 6826 df-wrecs 7059 df-recs 7121 df-rdg 7159 df-1o 7213 df-oadd 7217 df-er 7394 df-en 7601 df-dom 7602 df-sdom 7603 df-fin 7604 df-card 8404 df-cda 8629 df-pnf 9708 df-mnf 9709 df-xr 9710 df-ltxr 9711 df-le 9712 df-sub 9893 df-neg 9894 df-nn 10643 df-2 10701 df-n0 10904 df-z 10972 df-uz 11194 df-fz 11820 df-fzo 11953 df-hash 12554 df-word 12703 df-lsw 12704 df-usgra 25116

This theorem is referenced by: clwlkisclwwlklem2 25570

W3C validator