eclclwwlkn1

Description: An equivalence class according to .~ . (Contributed by Alexander van der Vekens, 12-Apr-2018) (Revised by AV, 30-Apr-2021)

	Ref	Expression
Hypotheses	erclwwlkn.w	$⊢ W = N ClWWalksN G$
	erclwwlkn.r	$⊢ \underset{˙}{\sim} = \{⟨t, u⟩ \| (t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
Assertion	eclclwwlkn1	$⊢ B \in X \to (B \in (W / \underset{˙}{\sim}) \leftrightarrow \exists x \in W B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$

Proof

Step	Hyp	Ref	Expression
1		erclwwlkn.w	$⊢ W = N ClWWalksN G$
2		erclwwlkn.r	$⊢ \underset{˙}{\sim} = \{⟨t, u⟩ \| (t \in W \land u \in W \land \exists n \in (0 \dots N) t = u cyclShift n)\}$
3		elqsecl	$⊢ B \in X \to (B \in (W / \underset{˙}{\sim}) \leftrightarrow \exists x \in W B = \{y \| x \underset{˙}{\sim} y\})$
4	1 2	erclwwlknsym	$⊢ x \underset{˙}{\sim} y \to y \underset{˙}{\sim} x$
5	1 2	erclwwlknsym	$⊢ y \underset{˙}{\sim} x \to x \underset{˙}{\sim} y$
6	4 5	impbii	$⊢ x \underset{˙}{\sim} y \leftrightarrow y \underset{˙}{\sim} x$
7	6	a1i	$⊢ (B \in X \land x \in W) \to (x \underset{˙}{\sim} y \leftrightarrow y \underset{˙}{\sim} x)$
8	7	abbidv	$⊢ (B \in X \land x \in W) \to \{y \| x \underset{˙}{\sim} y\} = \{y \| y \underset{˙}{\sim} x\}$
9	1 2	erclwwlkneq	$⊢ (y \in V \land x \in V) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
10	9	el2v	$⊢ y \underset{˙}{\sim} x \leftrightarrow (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n)$
11	10	a1i	$⊢ (B \in X \land x \in W) \to (y \underset{˙}{\sim} x \leftrightarrow (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
12	11	abbidv	$⊢ (B \in X \land x \in W) \to \{y \| y \underset{˙}{\sim} x\} = \{y \| (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n)\}$
13		3anan12	$⊢ (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n) \leftrightarrow (x \in W \land (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
14		ibar	$⊢ x \in W \to ((y \in W \land \exists n \in (0 \dots N) y = x cyclShift n) \leftrightarrow (x \in W \land (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n)))$
15	14	bicomd	$⊢ x \in W \to ((x \in W \land (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n)) \leftrightarrow (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
16	15	adantl	$⊢ (B \in X \land x \in W) \to ((x \in W \land (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n)) \leftrightarrow (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
17	13 16	bitrid	$⊢ (B \in X \land x \in W) \to ((y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n) \leftrightarrow (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n))$
18	17	abbidv	$⊢ (B \in X \land x \in W) \to \{y \| (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n)\} = \{y \| (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n)\}$
19		df-rab	$⊢ \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} = \{y \| (y \in W \land \exists n \in (0 \dots N) y = x cyclShift n)\}$
20	18 19	eqtr4di	$⊢ (B \in X \land x \in W) \to \{y \| (y \in W \land x \in W \land \exists n \in (0 \dots N) y = x cyclShift n)\} = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}$
21	8 12 20	3eqtrd	$⊢ (B \in X \land x \in W) \to \{y \| x \underset{˙}{\sim} y\} = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}$
22	21	eqeq2d	$⊢ (B \in X \land x \in W) \to (B = \{y \| x \underset{˙}{\sim} y\} \leftrightarrow B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$
23	22	rexbidva	$⊢ B \in X \to (\exists x \in W B = \{y \| x \underset{˙}{\sim} y\} \leftrightarrow \exists x \in W B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$
24	3 23	bitrd	$⊢ B \in X \to (B \in (W / \underset{˙}{\sim}) \leftrightarrow \exists x \in W B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$

Metamath Proof Explorer

Theorem eclclwwlkn1

Proof