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 ) ”⟩ ) ⟩ ∈ 𝐶 )