Metamath Proof Explorer

Theorem clwlkclwwlkfolem

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

Ref Expression
Hypothesis clwlkclwwlkf.c ${⊢}{C}=\left\{{w}\in \mathrm{ClWalks}\left({G}\right)|1\le \left|{1}^{st}\left({w}\right)\right|\right\}$
Assertion clwlkclwwlkfolem ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\wedge ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\right)\to ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in {C}$

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ${⊢}{C}=\left\{{w}\in \mathrm{ClWalks}\left({G}\right)|1\le \left|{1}^{st}\left({w}\right)\right|\right\}$
2 simp3 ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\wedge ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\right)\to ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)$
3 wrdlenccats1lenm1 ${⊢}{W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1=\left|{W}\right|$
4 3 eqcomd ${⊢}{W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left|{W}\right|=\left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
5 4 breq2d ${⊢}{W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\to \left(1\le \left|{W}\right|↔1\le \left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1\right)$
6 5 biimpa ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\right)\to 1\le \left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
7 6 3adant3 ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\wedge ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\right)\to 1\le \left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
8 df-br ${⊢}{f}\mathrm{ClWalks}\left({G}\right)\left({W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right)↔⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)$
9 clwlkiswlk ${⊢}{f}\mathrm{ClWalks}\left({G}\right)\left({W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right)\to {f}\mathrm{Walks}\left({G}\right)\left({W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right)$
10 wlklenvm1 ${⊢}{f}\mathrm{Walks}\left({G}\right)\left({W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right)\to \left|{f}\right|=\left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
11 9 10 syl ${⊢}{f}\mathrm{ClWalks}\left({G}\right)\left({W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right)\to \left|{f}\right|=\left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
12 8 11 sylbir ${⊢}⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\to \left|{f}\right|=\left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
13 12 3ad2ant3 ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\wedge ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\right)\to \left|{f}\right|=\left|{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\right|-1$
14 7 13 breqtrrd ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\wedge ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\right)\to 1\le \left|{f}\right|$
15 vex ${⊢}{f}\in \mathrm{V}$
16 ovex ${⊢}{W}\mathrm{++}⟨“{W}\left(0\right)”⟩\in \mathrm{V}$
17 15 16 op1std ${⊢}{c}=⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\to {1}^{st}\left({c}\right)={f}$
18 17 fveq2d ${⊢}{c}=⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\to \left|{1}^{st}\left({c}\right)\right|=\left|{f}\right|$
19 18 breq2d ${⊢}{c}=⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\to \left(1\le \left|{1}^{st}\left({c}\right)\right|↔1\le \left|{f}\right|\right)$
20 2fveq3 ${⊢}{w}={c}\to \left|{1}^{st}\left({w}\right)\right|=\left|{1}^{st}\left({c}\right)\right|$
21 20 breq2d ${⊢}{w}={c}\to \left(1\le \left|{1}^{st}\left({w}\right)\right|↔1\le \left|{1}^{st}\left({c}\right)\right|\right)$
22 21 cbvrabv ${⊢}\left\{{w}\in \mathrm{ClWalks}\left({G}\right)|1\le \left|{1}^{st}\left({w}\right)\right|\right\}=\left\{{c}\in \mathrm{ClWalks}\left({G}\right)|1\le \left|{1}^{st}\left({c}\right)\right|\right\}$
23 1 22 eqtri ${⊢}{C}=\left\{{c}\in \mathrm{ClWalks}\left({G}\right)|1\le \left|{1}^{st}\left({c}\right)\right|\right\}$
24 19 23 elrab2 ${⊢}⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in {C}↔\left(⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\wedge 1\le \left|{f}\right|\right)$
25 2 14 24 sylanbrc ${⊢}\left({W}\in \mathrm{Word}\mathrm{Vtx}\left({G}\right)\wedge 1\le \left|{W}\right|\wedge ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in \mathrm{ClWalks}\left({G}\right)\right)\to ⟨{f},{W}\mathrm{++}⟨“{W}\left(0\right)”⟩⟩\in {C}$