eleclclwwlkn

Description: A member of an equivalence class according to .~ . (Contributed by Alexander van der Vekens, 11-May-2018) (Revised by AV, 1-May-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	eleclclwwlkn	$⊢ (B \in (W / \underset{˙}{\sim}) \land X \in B) \to (Y \in B \leftrightarrow (Y \in W \land \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	1 2	eclclwwlkn1	$⊢ B \in (W / \underset{˙}{\sim}) \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\})$
4		eqeq1	$⊢ y = Y \to (y = x cyclShift n \leftrightarrow Y = x cyclShift n)$
5	4	rexbidv	$⊢ y = Y \to (\exists n \in (0 \dots N) y = x cyclShift n \leftrightarrow \exists n \in (0 \dots N) Y = x cyclShift n)$
6	5	elrab	$⊢ Y \in \{y \in W \| \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)$
7		oveq2	$⊢ n = k \to x cyclShift n = x cyclShift k$
8	7	eqeq2d	$⊢ n = k \to (Y = x cyclShift n \leftrightarrow Y = x cyclShift k)$
9	8	cbvrexvw	$⊢ \exists n \in (0 \dots N) Y = x cyclShift n \leftrightarrow \exists k \in (0 \dots N) Y = x cyclShift k$
10		eqeq1	$⊢ y = X \to (y = x cyclShift n \leftrightarrow X = x cyclShift n)$
11	10	rexbidv	$⊢ y = X \to (\exists n \in (0 \dots N) y = x cyclShift n \leftrightarrow \exists n \in (0 \dots N) X = x cyclShift n)$
12	11	elrab	$⊢ X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \leftrightarrow (X \in W \land \exists n \in (0 \dots N) X = x cyclShift n)$
13		oveq2	$⊢ n = m \to x cyclShift n = x cyclShift m$
14	13	eqeq2d	$⊢ n = m \to (X = x cyclShift n \leftrightarrow X = x cyclShift m)$
15	14	cbvrexvw	$⊢ \exists n \in (0 \dots N) X = x cyclShift n \leftrightarrow \exists m \in (0 \dots N) X = x cyclShift m$
16	1	eleclclwwlknlem2	$⊢ ((m \in (0 \dots N) \land X = x cyclShift m) \land (X \in W \land x \in W)) \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$
17	16	ex	$⊢ (m \in (0 \dots N) \land X = x cyclShift m) \to ((X \in W \land x \in W) \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
18	17	rexlimiva	$⊢ \exists m \in (0 \dots N) X = x cyclShift m \to ((X \in W \land x \in W) \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
19	15 18	sylbi	$⊢ \exists n \in (0 \dots N) X = x cyclShift n \to ((X \in W \land x \in W) \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
20	19	expd	$⊢ \exists n \in (0 \dots N) X = x cyclShift n \to (X \in W \to (x \in W \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)))$
21	20	impcom	$⊢ (X \in W \land \exists n \in (0 \dots N) X = x cyclShift n) \to (x \in W \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
22	12 21	sylbi	$⊢ X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (x \in W \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
23	22	com12	$⊢ x \in W \to (X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
24	23	ad2antlr	$⊢ ((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to (X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n))$
25	24	imp	$⊢ (((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \land X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to (\exists k \in (0 \dots N) Y = x cyclShift k \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$
26	9 25	syl5bb	$⊢ (((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \land X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to (\exists n \in (0 \dots N) Y = x cyclShift n \leftrightarrow \exists n \in (0 \dots N) Y = X cyclShift n)$
27	26	anbi2d	$⊢ (((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \land X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to ((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))$
28	6 27	syl5bb	$⊢ (((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \land X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to (Y \in \{y \in W \| \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))$
29	28	ex	$⊢ ((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to (X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (Y \in \{y \in W \| \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)))$
30		eleq2	$⊢ B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (X \in B \leftrightarrow X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$
31		eleq2	$⊢ B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (Y \in B \leftrightarrow Y \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\})$
32	31	bibi1d	$⊢ B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to ((Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n)) \leftrightarrow (Y \in \{y \in W \| \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)))$
33	30 32	imbi12d	$⊢ B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to ((X \in B \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n))) \leftrightarrow (X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (Y \in \{y \in W \| \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))))$
34	33	adantl	$⊢ ((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to ((X \in B \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n))) \leftrightarrow (X \in \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (Y \in \{y \in W \| \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))))$
35	29 34	mpbird	$⊢ ((B \in (W / \underset{˙}{\sim}) \land x \in W) \land B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\}) \to (X \in B \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n)))$
36	35	rexlimdva2	$⊢ B \in (W / \underset{˙}{\sim}) \to (\exists x \in W B = \{y \in W \| \exists n \in (0 \dots N) y = x cyclShift n\} \to (X \in B \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n))))$
37	3 36	sylbid	$⊢ B \in (W / \underset{˙}{\sim}) \to (B \in (W / \underset{˙}{\sim}) \to (X \in B \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n))))$
38	37	pm2.43i	$⊢ B \in (W / \underset{˙}{\sim}) \to (X \in B \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n)))$
39	38	imp	$⊢ (B \in (W / \underset{˙}{\sim}) \land X \in B) \to (Y \in B \leftrightarrow (Y \in W \land \exists n \in (0 \dots N) Y = X cyclShift n))$

Metamath Proof Explorer

Theorem eleclclwwlkn

Proof