Theorem clwlkclwwlkflem

Description: Lemma for clwlkclwwlkf . (Contributed by AV, 24-May-2022)

	Ref	Expression
Hypotheses	clwlkclwwlkf.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
	clwlkclwwlkf.a	⊢ 𝐴 = ( 1st ‘ 𝑈 )
	clwlkclwwlkf.b	⊢ 𝐵 = ( 2nd ‘ 𝑈 )
Assertion	clwlkclwwlkflem	⊢ ( 𝑈 ∈ 𝐶 → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		clwlkclwwlkf.c	⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
2		clwlkclwwlkf.a	⊢ 𝐴 = ( 1st ‘ 𝑈 )
3		clwlkclwwlkf.b	⊢ 𝐵 = ( 2nd ‘ 𝑈 )
4		fveq2	⊢ ( 𝑤 = 𝑈 → ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑈 ) )
5	4 2	eqtr4di	⊢ ( 𝑤 = 𝑈 → ( 1st ‘ 𝑤 ) = 𝐴 )
6	5	fveq2d	⊢ ( 𝑤 = 𝑈 → ( ♯ ‘ ( 1st ‘ 𝑤 ) ) = ( ♯ ‘ 𝐴 ) )
7	6	breq2d	⊢ ( 𝑤 = 𝑈 → ( 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) ↔ 1 ≤ ( ♯ ‘ 𝐴 ) ) )
8	7 1	elrab2	⊢ ( 𝑈 ∈ 𝐶 ↔ ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) )
9		clwlkwlk	⊢ ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) → 𝑈 ∈ ( Walks ‘ 𝐺 ) )
10		wlkop	⊢ ( 𝑈 ∈ ( Walks ‘ 𝐺 ) → 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ )
11	2 3	opeq12i	⊢ ⟨ 𝐴 , 𝐵 ⟩ = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩
12	11	eqeq2i	⊢ ( 𝑈 = ⟨ 𝐴 , 𝐵 ⟩ ↔ 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ )
13		eleq1	⊢ ( 𝑈 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ClWalks ‘ 𝐺 ) ) )
14		df-br	⊢ ( 𝐴 ( ClWalks ‘ 𝐺 ) 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ClWalks ‘ 𝐺 ) )
15		isclwlk	⊢ ( 𝐴 ( ClWalks ‘ 𝐺 ) 𝐵 ↔ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) )
16		wlkcl	⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
17		elnnnn0c	⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) )
18	17	a1i	⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) ) )
19	16 18	mpbirand	⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( ( ♯ ‘ 𝐴 ) ∈ ℕ ↔ 1 ≤ ( ♯ ‘ 𝐴 ) ) )
20	19	bicomd	⊢ ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 → ( 1 ≤ ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
21	20	adantr	⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
22	21	pm5.32i	⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) ↔ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
23		df-3an	⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ↔ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
24	22 23	sylbb2	⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
25	24	ex	⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) )
26	15 25	sylbi	⊢ ( 𝐴 ( ClWalks ‘ 𝐺 ) 𝐵 → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) )
27	14 26	sylbir	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ClWalks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) )
28	13 27	syl6bi	⊢ ( 𝑈 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) ) )
29	12 28	sylbir	⊢ ( 𝑈 = ⟨ ( 1st ‘ 𝑈 ) , ( 2nd ‘ 𝑈 ) ⟩ → ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) ) )
30	10 29	syl	⊢ ( 𝑈 ∈ ( Walks ‘ 𝐺 ) → ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) ) )
31	9 30	mpcom	⊢ ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) → ( 1 ≤ ( ♯ ‘ 𝐴 ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ) )
32	31	imp	⊢ ( ( 𝑈 ∈ ( ClWalks ‘ 𝐺 ) ∧ 1 ≤ ( ♯ ‘ 𝐴 ) ) → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
33	8 32	sylbi	⊢ ( 𝑈 ∈ 𝐶 → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )