This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clwlkclwwlkfolem

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

Ref Expression
Hypothesis clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
Assertion clwlkclwwlkfolem ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ∧ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
2 simp3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ∧ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
3 wrdlenccats1lenm1 ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) = ( ♯ ‘ 𝑊 ) )
4 3 eqcomd ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( ♯ ‘ 𝑊 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
5 4 breq2d ⊢ ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝑊 ) ↔ 1 ≤ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) ) )
6 5 biimpa ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ) → 1 ≤ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
7 6 3adant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ∧ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → 1 ≤ ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
8 df-br ⊢ ( 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ↔ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
9 clwlkiswlk ⊢ ( 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → 𝑓 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) )
10 wlklenvm1 ⊢ ( 𝑓 ( Walks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
11 9 10 syl ⊢ ( 𝑓 ( ClWalks ‘ 𝐺 ) ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
12 8 11 sylbir ⊢ ( ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
13 12 3ad2ant3 ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ∧ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ( ♯ ‘ 𝑓 ) = ( ( ♯ ‘ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ) − 1 ) )
14 7 13 breqtrrd ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ∧ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → 1 ≤ ( ♯ ‘ 𝑓 ) )
15 vex ⊢ 𝑓 ∈ V
16 ovex ⊢ ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ∈ V
17 15 16 op1std ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ → ( 1st ‘ 𝑐 ) = 𝑓 )
18 17 fveq2d ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ → ( ♯ ‘ ( 1st ‘ 𝑐 ) ) = ( ♯ ‘ 𝑓 ) )
19 18 breq2d ⊢ ( 𝑐 = ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ → ( 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ↔ 1 ≤ ( ♯ ‘ 𝑓 ) ) )
20 2fveq3 ⊢ ( 𝑤 = 𝑐 → ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( ♯ ‘ ( 1st ‘ 𝑐 ) ) )
21 20 breq2d ⊢ ( 𝑤 = 𝑐 → ( 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) ↔ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) ) )
22 21 cbvrabv ⊢ { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) } = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) }
23 1 22 eqtri ⊢ 𝐶 = { 𝑐 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑐 ) ) }
24 19 23 elrab2 ⊢ ( ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 ↔ ( ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑓 ) ) )
25 2 14 24 sylanbrc ⊢ ( ( 𝑊 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝑊 ) ∧ ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) → ⟨ 𝑓 , ( 𝑊 ++ ⟨“ ( 𝑊 ‘ 0 ) ”⟩ ) ⟩ ∈ 𝐶 )