erclwwlktr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > erclwwlktr		Structured version Visualization version GIF version

Theorem erclwwlktr 29784

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.)

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

**Assertion**
Ref	Expression
erclwwlktr	⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)

Distinct variable groups: 𝑛,𝐺,𝑢,𝑤 𝑥,𝑛,𝑢,𝑤,𝑦 𝑧,𝑛,𝑢,𝑤,𝑥 Allowed substitution hints: ∼ (𝑥,𝑦,𝑧,𝑤,𝑢,𝑛) 𝐺(𝑥,𝑦,𝑧)

Proof of Theorem erclwwlktr Dummy variables 𝑚 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3472	. 2 ⊢ 𝑥 ∈ V
2		vex 3472	. 2 ⊢ 𝑦 ∈ V
3		vex 3472	. 2 ⊢ 𝑧 ∈ V
4		erclwwlk.r	. . . . . 6 ⊢ ∼ = {⟨𝑢, 𝑤⟩ ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))}
5	4	erclwwlkeqlen 29781	. . . . 5 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 → (♯‘𝑥) = (♯‘𝑦)))
6	5	3adant3 1129	. . . 4 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (♯‘𝑥) = (♯‘𝑦)))
7	4	erclwwlkeqlen 29781	. . . . . . 7 ⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (♯‘𝑦) = (♯‘𝑧)))
8	7	3adant1 1127	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → (♯‘𝑦) = (♯‘𝑧)))
9	4	erclwwlkeq 29780	. . . . . . . 8 ⊢ ((𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))))
10	9	3adant1 1127	. . . . . . 7 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 ↔ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))))
11	4	erclwwlkeq 29780	. . . . . . . . . 10 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))))
12	11	3adant3 1129	. . . . . . . . 9 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 ↔ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))))
13		simpr1 1191	. . . . . . . . . . . . . . 15 ⊢ (((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → 𝑥 ∈ (ClWWalks‘𝐺))
14		simplr2 1213	. . . . . . . . . . . . . . 15 ⊢ (((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → 𝑧 ∈ (ClWWalks‘𝐺))
15		oveq2 7413	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑚 → (𝑦 cyclShift 𝑛) = (𝑦 cyclShift 𝑚))
16	15	eqeq2d 2737	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑚 → (𝑥 = (𝑦 cyclShift 𝑛) ↔ 𝑥 = (𝑦 cyclShift 𝑚)))
17	16	cbvrexvw 3229	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) ↔ ∃𝑚 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑚))
18		oveq2 7413	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑛 = 𝑘 → (𝑧 cyclShift 𝑛) = (𝑧 cyclShift 𝑘))
19	18	eqeq2d 2737	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛 = 𝑘 → (𝑦 = (𝑧 cyclShift 𝑛) ↔ 𝑦 = (𝑧 cyclShift 𝑘)))
20	19	cbvrexvw 3229	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) ↔ ∃𝑘 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑘))
21		eqid 2726	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (Vtx‘𝐺) = (Vtx‘𝐺)
22	21	clwwlkbp 29747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑧 ∈ (ClWWalks‘𝐺) → (𝐺 ∈ V ∧ 𝑧 ∈ Word (Vtx‘𝐺) ∧ 𝑧 ≠ ∅))
23	22	simp2d 1140	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑧 ∈ (ClWWalks‘𝐺) → 𝑧 ∈ Word (Vtx‘𝐺))
24	23	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → 𝑧 ∈ Word (Vtx‘𝐺))
25		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)))
26	24, 25	cshwcsh2id 14785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → (((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
27	26	exp5l 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → (𝑚 ∈ (0...(♯‘𝑦)) → (𝑥 = (𝑦 cyclShift 𝑚) → (𝑘 ∈ (0...(♯‘𝑧)) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))))
28	27	imp41 425	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) ∧ 𝑚 ∈ (0...(♯‘𝑦))) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ 𝑘 ∈ (0...(♯‘𝑧))) → (𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
29	28	rexlimdva 3149	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) ∧ 𝑚 ∈ (0...(♯‘𝑦))) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → (∃𝑘 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
30	29	rexlimdva2 3151	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → (∃𝑚 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑘 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑘) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
31	20, 30	syl7bi 255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → (∃𝑚 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑚) → (∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
32	17, 31	biimtrid 241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) ∧ 𝑧 ∈ (ClWWalks‘𝐺)) ∧ ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦))) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
33	32	exp31 419	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) → (𝑧 ∈ (ClWWalks‘𝐺) → (((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → (∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))))
34	33	com15 101	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛) → (𝑧 ∈ (ClWWalks‘𝐺) → (((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))))
35	34	impcom 407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → (((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))
36	35	3adant1 1127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → (((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))))
37	36	impcom 407	. . . . . . . . . . . . . . . . . 18 ⊢ ((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
38	37	com13 88	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺)) → (∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛) → ((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
39	38	3impia 1114	. . . . . . . . . . . . . . . 16 ⊢ ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
40	39	impcom 407	. . . . . . . . . . . . . . 15 ⊢ (((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))
41	13, 14, 40	3jca 1125	. . . . . . . . . . . . . 14 ⊢ (((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
42	4	erclwwlkeq 29780	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
43	42	3adant2 1128	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑧 ↔ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))))
44	41, 43	syl5ibrcom 246	. . . . . . . . . . . . 13 ⊢ (((((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) ∧ (𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛))) ∧ (𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛))) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧))
45	44	exp31 419	. . . . . . . . . . . 12 ⊢ (((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) → ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → 𝑥 ∼ 𝑧))))
46	45	com24 95	. . . . . . . . . . 11 ⊢ (((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧))))
47	46	ex 412	. . . . . . . . . 10 ⊢ ((♯‘𝑦) = (♯‘𝑧) → ((♯‘𝑥) = (♯‘𝑦) → ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧)))))
48	47	com4t 93	. . . . . . . . 9 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∈ (ClWWalks‘𝐺) ∧ 𝑦 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑦))𝑥 = (𝑦 cyclShift 𝑛)) → ((♯‘𝑦) = (♯‘𝑧) → ((♯‘𝑥) = (♯‘𝑦) → ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧)))))
49	12, 48	sylbid 239	. . . . . . . 8 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((♯‘𝑦) = (♯‘𝑧) → ((♯‘𝑥) = (♯‘𝑦) → ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → 𝑥 ∼ 𝑧)))))
50	49	com25 99	. . . . . . 7 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑦 ∈ (ClWWalks‘𝐺) ∧ 𝑧 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(♯‘𝑧))𝑦 = (𝑧 cyclShift 𝑛)) → ((♯‘𝑦) = (♯‘𝑧) → ((♯‘𝑥) = (♯‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧)))))
51	10, 50	sylbid 239	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((♯‘𝑦) = (♯‘𝑧) → ((♯‘𝑥) = (♯‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧)))))
52	8, 51	mpdd 43	. . . . 5 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑦 ∼ 𝑧 → ((♯‘𝑥) = (♯‘𝑦) → (𝑥 ∼ 𝑦 → 𝑥 ∼ 𝑧))))
53	52	com24 95	. . . 4 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → ((♯‘𝑥) = (♯‘𝑦) → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧))))
54	6, 53	mpdd 43	. . 3 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → (𝑥 ∼ 𝑦 → (𝑦 ∼ 𝑧 → 𝑥 ∼ 𝑧)))
55	54	impd 410	. 2 ⊢ ((𝑥 ∈ V ∧ 𝑦 ∈ V ∧ 𝑧 ∈ V) → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧))
56	1, 2, 3, 55	mp3an 1457	1 ⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ≠ wne 2934 ∃wrex 3064 Vcvv 3468 ∅c0 4317 class class class wbr 5141 {copab 5203 ‘cfv 6537 (class class class)co 7405 0cc0 11112 ...cfz 13490 ♯chash 14295 Word cword 14470 cyclShift ccsh 14744 Vtxcvtx 28764 ClWWalkscclwwlk 29743

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2697 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5356 ax-pr 5420 ax-un 7722 ax-cnex 11168 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 ax-pre-sup 11190

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2704 df-cleq 2718 df-clel 2804 df-nfc 2879 df-ne 2935 df-nel 3041 df-ral 3056 df-rex 3065 df-rmo 3370 df-reu 3371 df-rab 3427 df-v 3470 df-sbc 3773 df-csb 3889 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-int 4944 df-iun 4992 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5567 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-xp 5675 df-rel 5676 df-cnv 5677 df-co 5678 df-dm 5679 df-rn 5680 df-res 5681 df-ima 5682 df-pred 6294 df-ord 6361 df-on 6362 df-lim 6363 df-suc 6364 df-iota 6489 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7361 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7853 df-1st 7974 df-2nd 7975 df-frecs 8267 df-wrecs 8298 df-recs 8372 df-rdg 8411 df-1o 8467 df-er 8705 df-map 8824 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9439 df-inf 9440 df-card 9936 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 df-nn 12217 df-2 12279 df-n0 12477 df-z 12563 df-uz 12827 df-rp 12981 df-fz 13491 df-fzo 13634 df-fl 13763 df-mod 13841 df-hash 14296 df-word 14471 df-concat 14527 df-substr 14597 df-pfx 14627 df-csh 14745 df-clwwlk 29744

This theorem is referenced by: erclwwlk 29785

W3C validator