Metamath Proof Explorer

Theorem clwlkclwwlkfolem

Description: Lemma for clwlkclwwlkfo . (Contributed by AV, 25-May-2022)

Ref Expression
Hypothesis clwlkclwwlkf.c ⊢C=w∈ClWalks⁡G|1≤1st⁡w
Assertion clwlkclwwlkfolem ⊢W∈WordVtx⁡G∧1≤W∧fW++⟨“W⁡0”⟩∈ClWalks⁡G→fW++⟨“W⁡0”⟩∈C

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢C=w∈ClWalks⁡G|1≤1st⁡w
2 simp3 ⊢W∈WordVtx⁡G∧1≤W∧fW++⟨“W⁡0”⟩∈ClWalks⁡G→fW++⟨“W⁡0”⟩∈ClWalks⁡G
3 wrdlenccats1lenm1 ⊢W∈WordVtx⁡G→W++⟨“W⁡0”⟩−1=W
4 3 eqcomd ⊢W∈WordVtx⁡G→W=W++⟨“W⁡0”⟩−1
5 4 breq2d ⊢W∈WordVtx⁡G→1≤W↔1≤W++⟨“W⁡0”⟩−1
6 5 biimpa ⊢W∈WordVtx⁡G∧1≤W→1≤W++⟨“W⁡0”⟩−1
7 6 3adant3 ⊢W∈WordVtx⁡G∧1≤W∧fW++⟨“W⁡0”⟩∈ClWalks⁡G→1≤W++⟨“W⁡0”⟩−1
8 df-br ⊢fClWalks⁡GW++⟨“W⁡0”⟩↔fW++⟨“W⁡0”⟩∈ClWalks⁡G
9 clwlkiswlk ⊢fClWalks⁡GW++⟨“W⁡0”⟩→fWalks⁡GW++⟨“W⁡0”⟩
10 wlklenvm1 ⊢fWalks⁡GW++⟨“W⁡0”⟩→f=W++⟨“W⁡0”⟩−1
11 9 10 syl ⊢fClWalks⁡GW++⟨“W⁡0”⟩→f=W++⟨“W⁡0”⟩−1
12 8 11 sylbir ⊢fW++⟨“W⁡0”⟩∈ClWalks⁡G→f=W++⟨“W⁡0”⟩−1
13 12 3ad2ant3 ⊢W∈WordVtx⁡G∧1≤W∧fW++⟨“W⁡0”⟩∈ClWalks⁡G→f=W++⟨“W⁡0”⟩−1
14 7 13 breqtrrd ⊢W∈WordVtx⁡G∧1≤W∧fW++⟨“W⁡0”⟩∈ClWalks⁡G→1≤f
15 vex ⊢f∈V
16 ovex ⊢W++⟨“W⁡0”⟩∈V
17 15 16 op1std ⊢c=fW++⟨“W⁡0”⟩→1st⁡c=f
18 17 fveq2d ⊢c=fW++⟨“W⁡0”⟩→1st⁡c=f
19 18 breq2d ⊢c=fW++⟨“W⁡0”⟩→1≤1st⁡c↔1≤f
20 2fveq3 ⊢w=c→1st⁡w=1st⁡c
21 20 breq2d ⊢w=c→1≤1st⁡w↔1≤1st⁡c
22 21 cbvrabv ⊢w∈ClWalks⁡G|1≤1st⁡w=c∈ClWalks⁡G|1≤1st⁡c
23 1 22 eqtri ⊢C=c∈ClWalks⁡G|1≤1st⁡c
24 19 23 elrab2 ⊢fW++⟨“W⁡0”⟩∈C↔fW++⟨“W⁡0”⟩∈ClWalks⁡G∧1≤f
25 2 14 24 sylanbrc ⊢W∈WordVtx⁡G∧1≤W∧fW++⟨“W⁡0”⟩∈ClWalks⁡G→fW++⟨“W⁡0”⟩∈C