Metamath Proof Explorer

Theorem clwlkclwwlkf1lem3

Description: Lemma 3 for clwlkclwwlkf1 . (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 30-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
clwlkclwwlkf.a ⊢ 𝐴 = ( 1st ‘ 𝑈 )
clwlkclwwlkf.b ⊢ 𝐵 = ( 2nd ‘ 𝑈 )
clwlkclwwlkf.d ⊢ 𝐷 = ( 1st ‘ 𝑊 )
clwlkclwwlkf.e ⊢ 𝐸 = ( 2nd ‘ 𝑊 )
Assertion clwlkclwwlkf1lem3 ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c ⊢ 𝐶 = { 𝑤 ∈ ( ClWalks ‘ 𝐺 ) ∣ 1 ≤ ( ♯ ‘ ( 1st ‘ 𝑤 ) ) }
2 clwlkclwwlkf.a ⊢ 𝐴 = ( 1st ‘ 𝑈 )
3 clwlkclwwlkf.b ⊢ 𝐵 = ( 2nd ‘ 𝑈 )
4 clwlkclwwlkf.d ⊢ 𝐷 = ( 1st ‘ 𝑊 )
5 clwlkclwwlkf.e ⊢ 𝐸 = ( 2nd ‘ 𝑊 )
6 1 2 3 4 5 clwlkclwwlkf1lem2 ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) )
7 simprr ⊢ ( ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )
8 1 2 3 clwlkclwwlkflem ⊢ ( 𝑈 ∈ 𝐶 → ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) )
9 1 4 5 clwlkclwwlkflem ⊢ ( 𝑊 ∈ 𝐶 → ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) )
10 lbfzo0 ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ↔ ( ♯ ‘ 𝐴 ) ∈ ℕ )
11 10 biimpri ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
12 11 3ad2ant3 ⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
13 12 adantr ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
14 13 adantr ⊢ ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) → 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) )
15 fveq2 ⊢ ( 𝑖 = 0 → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ 0 ) )
16 fveq2 ⊢ ( 𝑖 = 0 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 0 ) )
17 15 16 eqeq12d ⊢ ( 𝑖 = 0 → ( ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ↔ ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ) )
18 17 rspcv ⊢ ( 0 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) → ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ) )
19 14 18 syl ⊢ ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) → ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ) )
20 simpl ⊢ ( ( ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) ∧ ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) )
21 eqtr ⊢ ( ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) → ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) )
22 21 adantl ⊢ ( ( ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) ∧ ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) → ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) )
23 20 22 eqtrd ⊢ ( ( ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) ∧ ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) )
24 23 exp32 ⊢ ( ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) )
25 24 com23 ⊢ ( ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐵 ‘ 0 ) → ( ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) )
26 25 eqcoms ⊢ ( ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) → ( ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) )
27 26 3ad2ant2 ⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) )
28 27 com12 ⊢ ( ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) → ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) )
29 28 3ad2ant2 ⊢ ( ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) → ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) ) )
30 29 impcom ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) )
31 30 adantr ⊢ ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ) )
32 31 imp ⊢ ( ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) ∧ ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) )
33 fveq2 ⊢ ( ( ♯ ‘ 𝐷 ) = ( ♯ ‘ 𝐴 ) → ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
34 33 eqcoms ⊢ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) → ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
35 34 adantl ⊢ ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) → ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
36 35 adantr ⊢ ( ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) ∧ ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ) → ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
37 32 36 eqtrd ⊢ ( ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) ∧ ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
38 37 ex ⊢ ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) → ( ( 𝐵 ‘ 0 ) = ( 𝐸 ‘ 0 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
39 19 38 syld ⊢ ( ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) ∧ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
40 39 ex ⊢ ( ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) ∧ ( 𝐷 ( Walks ‘ 𝐺 ) 𝐸 ∧ ( 𝐸 ‘ 0 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐷 ) ) ∧ ( ♯ ‘ 𝐷 ) ∈ ℕ ) ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) ) )
41 8 9 40 syl2an ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ) → ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) ) )
42 41 impd ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ) → ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
43 42 3adant3 ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
44 43 imp ⊢ ( ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) ) → ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
45 7 44 jca ⊢ ( ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) ∧ ( ( ♯ ‘ 𝐴 ) = ( ♯ ‘ 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ∧ ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
46 6 45 mpdan ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ∧ ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
47 fvex ⊢ ( ♯ ‘ 𝐴 ) ∈ V
48 fveq2 ⊢ ( 𝑖 = ( ♯ ‘ 𝐴 ) → ( 𝐵 ‘ 𝑖 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) )
49 fveq2 ⊢ ( 𝑖 = ( ♯ ‘ 𝐴 ) → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) )
50 48 49 eqeq12d ⊢ ( 𝑖 = ( ♯ ‘ 𝐴 ) → ( ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ↔ ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
51 50 ralunsn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ V → ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ∧ ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) ) )
52 47 51 ax-mp ⊢ ( ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ↔ ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ∧ ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) = ( 𝐸 ‘ ( ♯ ‘ 𝐴 ) ) ) )
53 46 52 sylibr ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )
54 nnnn0 ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
55 elnn0uz ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ0 ↔ ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
56 54 55 sylib ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
57 56 3ad2ant3 ⊢ ( ( 𝐴 ( Walks ‘ 𝐺 ) 𝐵 ∧ ( 𝐵 ‘ 0 ) = ( 𝐵 ‘ ( ♯ ‘ 𝐴 ) ) ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
58 8 57 syl ⊢ ( 𝑈 ∈ 𝐶 → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
59 58 3ad2ant1 ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) )
60 fzisfzounsn ⊢ ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 0 ) → ( 0 ... ( ♯ ‘ 𝐴 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
61 59 60 syl ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( 0 ... ( ♯ ‘ 𝐴 ) ) = ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) )
62 61 raleqdv ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ( ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ ( ( 0 ..^ ( ♯ ‘ 𝐴 ) ) ∪ { ( ♯ ‘ 𝐴 ) } ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) ) )
63 53 62 mpbird ⊢ ( ( 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶 ∧ ( 𝐵 prefix ( ♯ ‘ 𝐴 ) ) = ( 𝐸 prefix ( ♯ ‘ 𝐷 ) ) ) → ∀ 𝑖 ∈ ( 0 ... ( ♯ ‘ 𝐴 ) ) ( 𝐵 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )