Metamath Proof Explorer

Theorem erclwwlktr

Description: .~ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018) (Revised by AV, 30-Apr-2021)

Ref Expression
Hypothesis erclwwlk.r ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
Assertion erclwwlktr ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 )

Proof

Step Hyp Ref Expression
1 erclwwlk.r ⊢ ∼ = { ⟨ 𝑢 , 𝑤 ⟩ ∣ ( 𝑢 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑤 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑤 ) ) 𝑢 = ( 𝑤 cyclShift 𝑛 ) ) }
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 vex ⊢ 𝑧 ∈ V
5 1 erclwwlkeqlen ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
6 5 3adant3 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
7 1 erclwwlkeqlen ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ) )
8 7 3adant1 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ) )
9 1 erclwwlkeq ⊢ ( ( 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 ↔ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) )
10 9 3adant1 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 ↔ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) )
11 1 erclwwlkeq ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
12 11 3adant3 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) )
13 simpr1 ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) )
14 simplr2 ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) )
15 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑦 cyclShift 𝑛 ) = ( 𝑦 cyclShift 𝑚 ) )
16 15 eqeq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 = ( 𝑦 cyclShift 𝑛 ) ↔ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) )
17 16 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑚 ) )
18 oveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑧 cyclShift 𝑛 ) = ( 𝑧 cyclShift 𝑘 ) )
19 18 eqeq2d ⊢ ( 𝑛 = 𝑘 → ( 𝑦 = ( 𝑧 cyclShift 𝑛 ) ↔ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) )
20 19 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ↔ ∃ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) )
21 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
22 21 clwwlkbp ⊢ ( 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) → ( 𝐺 ∈ V ∧ 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) ∧ 𝑧 ≠ ∅ ) )
23 22 simp2d ⊢ ( 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) → 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) )
24 23 ad2antlr ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → 𝑧 ∈ Word ( Vtx ‘ 𝐺 ) )
25 simpr ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) )
26 24 25 cshwcsh2id ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ( ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ∧ 𝑦 = ( 𝑧 cyclShift 𝑘 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
27 26 exp5l ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) → ( 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) → ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) ) )
28 27 imp41 ⊢ ( ( ( ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) ∧ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) ) → ( 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
29 28 rexlimdva ⊢ ( ( ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) ) ∧ 𝑥 = ( 𝑦 cyclShift 𝑚 ) ) → ( ∃ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
30 29 rexlimdva2 ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( ∃ 𝑘 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑘 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
31 20 30 syl7bi ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑚 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑚 ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
32 17 31 syl5bi ⊢ ( ( ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ) ∧ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
33 32 exp31 ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) ) )
34 33 com15 ⊢ ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) → ( 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) ) )
35 34 impcom ⊢ ( ( 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) )
36 35 3adant1 ⊢ ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) ) )
37 36 impcom ⊢ ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
38 37 com13 ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ) → ( ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) → ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
39 38 3impia ⊢ ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
40 39 impcom ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) )
41 13 14 40 3jca ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) )
42 1 erclwwlkeq ⊢ ( ( 𝑥 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
43 42 3adant2 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑧 ↔ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑥 = ( 𝑧 cyclShift 𝑛 ) ) ) )
44 41 43 syl5ibrcom ⊢ ( ( ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) ∧ ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) ) ∧ ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → 𝑥 ∼ 𝑧 ) )
45 44 exp31 ⊢ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → 𝑥 ∼ 𝑧 ) ) ) )
46 45 com24 ⊢ ( ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) ∧ ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) )
47 46 ex ⊢ ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) ) )
48 47 com4t ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑦 ) ) 𝑥 = ( 𝑦 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) ) )
49 12 48 sylbid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → 𝑥 ∼ 𝑧 ) ) ) ) )
50 49 com25 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑦 ∈ ( ClWWalks ‘ 𝐺 ) ∧ 𝑧 ∈ ( ClWWalks ‘ 𝐺 ) ∧ ∃ 𝑛 ∈ ( 0 ... ( ♯ ‘ 𝑧 ) ) 𝑦 = ( 𝑧 cyclShift 𝑛 ) ) → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧 ) ) ) ) )
51 10 50 sylbid ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ( ♯ ‘ 𝑦 ) = ( ♯ ‘ 𝑧 ) → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧 ) ) ) ) )
52 8 51 mpdd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑦 ∼ 𝑧 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧 ) ) ) )
53 52 com24 ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) ) ) )
54 6 53 mpdd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( 𝑥 ∼ 𝑦 → ( 𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧 ) ) )
55 54 impd ⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V ) → ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 ) )
56 2 3 4 55 mp3an ⊢ ( ( 𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧 ) → 𝑥 ∼ 𝑧 )