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

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝑈 = ⟨ 𝐴 , 𝐵 ⟩ → ( 𝑈 ∈ ( 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 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )