pgnbgreunbgrlem4

	Ref	Expression
Hypotheses	pgnbgreunbgr.g	No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
	pgnbgreunbgr.v	$⊢ V = Vtx (G)$
	pgnbgreunbgr.e	$⊢ E = Edg (G)$
	pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
Assertion	pgnbgreunbgrlem4	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X \in V \land X = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$

Proof

Step	Hyp	Ref	Expression
1		pgnbgreunbgr.g	Could not format G = ( 5 gPetersenGr 2 ) : No typesetting found for \|- G = ( 5 gPetersenGr 2 ) with typecode \|-
2		pgnbgreunbgr.v	$⊢ V = Vtx (G)$
3		pgnbgreunbgr.e	$⊢ E = Edg (G)$
4		pgnbgreunbgr.n	$⊢ N = G NeighbVtx X$
5		1ex	$⊢ 1 \in V$
6		vex	$⊢ y \in V$
7	5 6	op2ndd	$⊢ X = ⟨1, y⟩ \to 2^{nd} (X) = y$
8		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) + 2 = y + 2$
9	8	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) + 2) \mod 5 = (y + 2) \mod 5$
10	9	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) + 2) \mod 5⟩ = ⟨1, (y + 2) \mod 5⟩$
11	10	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \leftrightarrow L = ⟨1, (y + 2) \mod 5⟩)$
12		opeq2	$⊢ 2^{nd} (X) = y \to ⟨0, 2^{nd} (X)⟩ = ⟨0, y⟩$
13	12	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨0, 2^{nd} (X)⟩ \leftrightarrow L = ⟨0, y⟩)$
14		oveq1	$⊢ 2^{nd} (X) = y \to 2^{nd} (X) - 2 = y - 2$
15	14	oveq1d	$⊢ 2^{nd} (X) = y \to (2^{nd} (X) - 2) \mod 5 = (y - 2) \mod 5$
16	15	opeq2d	$⊢ 2^{nd} (X) = y \to ⟨1, (2^{nd} (X) - 2) \mod 5⟩ = ⟨1, (y - 2) \mod 5⟩$
17	16	eqeq2d	$⊢ 2^{nd} (X) = y \to (L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \leftrightarrow L = ⟨1, (y - 2) \mod 5⟩)$
18	11 13 17	3orbi123d	$⊢ 2^{nd} (X) = y \to ((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \leftrightarrow (L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩))$
19	10	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \leftrightarrow K = ⟨1, (y + 2) \mod 5⟩)$
20	12	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨0, 2^{nd} (X)⟩ \leftrightarrow K = ⟨0, y⟩)$
21	16	eqeq2d	$⊢ 2^{nd} (X) = y \to (K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩ \leftrightarrow K = ⟨1, (y - 2) \mod 5⟩)$
22	19 20 21	3orbi123d	$⊢ 2^{nd} (X) = y \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \leftrightarrow (K = ⟨1, (y + 2) \mod 5⟩ \lor K = ⟨0, y⟩ \lor K = ⟨1, (y - 2) \mod 5⟩))$
23	18 22	anbi12d	$⊢ 2^{nd} (X) = y \to (((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \land (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩)) \leftrightarrow ((L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩) \land (K = ⟨1, (y + 2) \mod 5⟩ \lor K = ⟨0, y⟩ \lor K = ⟨1, (y - 2) \mod 5⟩)))$
24		simpr	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to K = ⟨1, (y + 2) \mod 5⟩$
25		simpl	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to L = ⟨1, (y + 2) \mod 5⟩$
26	24 25	neeq12d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to (K \neq L \leftrightarrow ⟨1, (y + 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩)$
27		eqid	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨1, (y + 2) \mod 5⟩$
28		eqneqall	$⊢ ⟨1, (y + 2) \mod 5⟩ = ⟨1, (y + 2) \mod 5⟩ \to (⟨1, (y + 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
29	27 28	ax-mp	$⊢ ⟨1, (y + 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
30	26 29	biimtrdi	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
31	30	impd	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
32	31	ex	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (K = ⟨1, (y + 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
33		prcom	$⊢ \{⟨1, b⟩, ⟨0, y⟩\} = \{⟨0, y⟩, ⟨1, b⟩\}$
34	33	eleq1i	$⊢ \{⟨1, b⟩, ⟨0, y⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨1, b⟩\} \in E$
35		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
36		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
37		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
38		eqid	$⊢ (0 ..^5) = (0 ..^5)$
39	37 38 1 3	gpgedgiov	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (y \in (0 ..^5) \land b \in (0 ..^5))) \to (\{⟨0, y⟩, ⟨1, b⟩\} \in E \leftrightarrow y = b)$
40	35 36 39	mpanl12	$⊢ (y \in (0 ..^5) \land b \in (0 ..^5)) \to (\{⟨0, y⟩, ⟨1, b⟩\} \in E \leftrightarrow y = b)$
41	40	ancoms	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨0, y⟩, ⟨1, b⟩\} \in E \leftrightarrow y = b)$
42	34 41	bitrid	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, b⟩, ⟨0, y⟩\} \in E \leftrightarrow y = b)$
43		opeq2	$⊢ y = b \to ⟨1, y⟩ = ⟨1, b⟩$
44	42 43	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, b⟩, ⟨0, y⟩\} \in E \to ⟨1, y⟩ = ⟨1, b⟩)$
45	44	adantld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
46		preq1	$⊢ K = ⟨1, (y + 2) \mod 5⟩ \to \{K, ⟨1, b⟩\} = \{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\}$
47	46	eleq1d	$⊢ K = ⟨1, (y + 2) \mod 5⟩ \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E)$
48		preq2	$⊢ L = ⟨0, y⟩ \to \{⟨1, b⟩, L\} = \{⟨1, b⟩, ⟨0, y⟩\}$
49	48	eleq1d	$⊢ L = ⟨0, y⟩ \to (\{⟨1, b⟩, L\} \in E \leftrightarrow \{⟨1, b⟩, ⟨0, y⟩\} \in E)$
50	47 49	bi2anan9r	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E))$
51	50	imbi1d	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩) \leftrightarrow ((\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
52	45 51	imbitrrid	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
53	52	adantld	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
54	53	ex	$⊢ L = ⟨0, y⟩ \to (K = ⟨1, (y + 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
55		prcom	$⊢ \{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} = \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\}$
56	55	eleq1i	$⊢ \{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E$
57		prcom	$⊢ \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} = \{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\}$
58	57	eleq1i	$⊢ \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E \leftrightarrow \{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E$
59	56 58	anbi12ci	$⊢ (\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \leftrightarrow (\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
60		5nn	$⊢ 5 \in ℕ$
61	60	nnzi	$⊢ 5 \in ℤ$
62		uzid	$⊢ 5 \in ℤ \to 5 \in ℤ_{\geq 5}$
63	61 62	ax-mp	$⊢ 5 \in ℤ_{\geq 5}$
64		4t2e8	$⊢ 4 \cdot 2 = 8$
65	64	oveq1i	$⊢ 4 \cdot 2 \mod 5 = 8 \mod 5$
66		8mod5e3	$⊢ 8 \mod 5 = 3$
67	65 66	eqtri	$⊢ 4 \cdot 2 \mod 5 = 3$
68		3ne0	$⊢ 3 \neq 0$
69	67 68	eqnetri	$⊢ 4 \cdot 2 \mod 5 \neq 0$
70	36 69	pm3.2i	$⊢ (2 \in (1 ..^⌈\frac{5}{2}⌉) \land 4 \cdot 2 \mod 5 \neq 0)$
71	37 38 1 3	gpgedg2iv	$⊢ (5 \in ℤ_{\geq 5} \land (b \in (0 ..^5) \land y \in (0 ..^5)) \land (2 \in (1 ..^⌈\frac{5}{2}⌉) \land 4 \cdot 2 \mod 5 \neq 0)) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \leftrightarrow b = y)$
72	63 70 71	mp3an13	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \leftrightarrow b = y)$
73	59 72	bitrid	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \leftrightarrow b = y)$
74	43	eqcoms	$⊢ b = y \to ⟨1, y⟩ = ⟨1, b⟩$
75	73 74	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
76		preq2	$⊢ L = ⟨1, (y - 2) \mod 5⟩ \to \{⟨1, b⟩, L\} = \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\}$
77	76	eleq1d	$⊢ L = ⟨1, (y - 2) \mod 5⟩ \to (\{⟨1, b⟩, L\} \in E \leftrightarrow \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E)$
78	47 77	bi2anan9r	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E))$
79	78	imbi1d	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩) \leftrightarrow ((\{⟨1, (y + 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
80	75 79	imbitrrid	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
81	80	adantld	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨1, (y + 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
82	81	ex	$⊢ L = ⟨1, (y - 2) \mod 5⟩ \to (K = ⟨1, (y + 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
83	32 54 82	3jaoi	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩) \to (K = ⟨1, (y + 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
84	41 43	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨0, y⟩, ⟨1, b⟩\} \in E \to ⟨1, y⟩ = ⟨1, b⟩)$
85	84	adantrd	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, y⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
86		preq1	$⊢ K = ⟨0, y⟩ \to \{K, ⟨1, b⟩\} = \{⟨0, y⟩, ⟨1, b⟩\}$
87	86	eleq1d	$⊢ K = ⟨0, y⟩ \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨1, b⟩\} \in E)$
88		preq2	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to \{⟨1, b⟩, L\} = \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\}$
89	88	eleq1d	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (\{⟨1, b⟩, L\} \in E \leftrightarrow \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E)$
90	87 89	bi2anan9r	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨0, y⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
91	90	imbi1d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩) \leftrightarrow ((\{⟨0, y⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
92	85 91	imbitrrid	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
93	92	adantld	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
94	93	ex	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (K = ⟨0, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
95		simpr	$⊢ (L = ⟨0, y⟩ \land K = ⟨0, y⟩) \to K = ⟨0, y⟩$
96		simpl	$⊢ (L = ⟨0, y⟩ \land K = ⟨0, y⟩) \to L = ⟨0, y⟩$
97	95 96	neeq12d	$⊢ (L = ⟨0, y⟩ \land K = ⟨0, y⟩) \to (K \neq L \leftrightarrow ⟨0, y⟩ \neq ⟨0, y⟩)$
98		eqid	$⊢ ⟨0, y⟩ = ⟨0, y⟩$
99		eqneqall	$⊢ ⟨0, y⟩ = ⟨0, y⟩ \to (⟨0, y⟩ \neq ⟨0, y⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
100	98 99	ax-mp	$⊢ ⟨0, y⟩ \neq ⟨0, y⟩ \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
101	97 100	biimtrdi	$⊢ (L = ⟨0, y⟩ \land K = ⟨0, y⟩) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
102	101	impd	$⊢ (L = ⟨0, y⟩ \land K = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
103	102	ex	$⊢ L = ⟨0, y⟩ \to (K = ⟨0, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
104	84	adantrd	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨0, y⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
105	86	adantl	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to \{K, ⟨1, b⟩\} = \{⟨0, y⟩, ⟨1, b⟩\}$
106	105	eleq1d	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨0, y⟩, ⟨1, b⟩\} \in E)$
107	76	adantr	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to \{⟨1, b⟩, L\} = \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\}$
108	107	eleq1d	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to (\{⟨1, b⟩, L\} \in E \leftrightarrow \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E)$
109	106 108	anbi12d	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨0, y⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E))$
110	109	imbi1d	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩) \leftrightarrow ((\{⟨0, y⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y - 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
111	104 110	imbitrrid	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
112	111	adantld	$⊢ (L = ⟨1, (y - 2) \mod 5⟩ \land K = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
113	112	ex	$⊢ L = ⟨1, (y - 2) \mod 5⟩ \to (K = ⟨0, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
114	94 103 113	3jaoi	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩) \to (K = ⟨0, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
115	66 68	eqnetri	$⊢ 8 \mod 5 \neq 0$
116	65 115	eqnetri	$⊢ 4 \cdot 2 \mod 5 \neq 0$
117		simpll	$⊢ ((5 \in ℤ_{\geq 5} \land 4 \cdot 2 \mod 5 \neq 0) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to 5 \in ℤ_{\geq 5}$
118		simpr	$⊢ ((5 \in ℤ_{\geq 5} \land 4 \cdot 2 \mod 5 \neq 0) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (b \in (0 ..^5) \land y \in (0 ..^5))$
119	36	a1i	$⊢ 5 \in ℤ_{\geq 5} \to 2 \in (1 ..^⌈\frac{5}{2}⌉)$
120	119	anim1i	$⊢ (5 \in ℤ_{\geq 5} \land 4 \cdot 2 \mod 5 \neq 0) \to (2 \in (1 ..^⌈\frac{5}{2}⌉) \land 4 \cdot 2 \mod 5 \neq 0)$
121	120	adantr	$⊢ ((5 \in ℤ_{\geq 5} \land 4 \cdot 2 \mod 5 \neq 0) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (2 \in (1 ..^⌈\frac{5}{2}⌉) \land 4 \cdot 2 \mod 5 \neq 0)$
122	117 118 121 71	syl3anc	$⊢ ((5 \in ℤ_{\geq 5} \land 4 \cdot 2 \mod 5 \neq 0) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \leftrightarrow b = y)$
123	63 116 122	mpanl12	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \leftrightarrow b = y)$
124	123 74	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
125	124	adantl	$⊢ (⟨1, (y - 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩ \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
126	125	a1i	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((⟨1, (y - 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩ \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
127		simpl	$⊢ (K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨1, (y + 2) \mod 5⟩) \to K = ⟨1, (y - 2) \mod 5⟩$
128		simpr	$⊢ (K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨1, (y + 2) \mod 5⟩) \to L = ⟨1, (y + 2) \mod 5⟩$
129	127 128	neeq12d	$⊢ (K = ⟨1, (y - 2) \mod 5⟩ \land L = ⟨1, (y + 2) \mod 5⟩) \to (K \neq L \leftrightarrow ⟨1, (y - 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩)$
130	129	ancoms	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (K \neq L \leftrightarrow ⟨1, (y - 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩)$
131	130	anbi1d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \leftrightarrow (⟨1, (y - 2) \mod 5⟩ \neq ⟨1, (y + 2) \mod 5⟩ \land (b \in (0 ..^5) \land y \in (0 ..^5))))$
132		preq1	$⊢ K = ⟨1, (y - 2) \mod 5⟩ \to \{K, ⟨1, b⟩\} = \{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\}$
133	132	eleq1d	$⊢ K = ⟨1, (y - 2) \mod 5⟩ \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E)$
134	133 89	bi2anan9r	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E))$
135	134	imbi1d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩) \leftrightarrow ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨1, (y + 2) \mod 5⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
136	126 131 135	3imtr4d	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
137	136	ex	$⊢ L = ⟨1, (y + 2) \mod 5⟩ \to (K = ⟨1, (y - 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
138	39	ancom2s	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, y⟩, ⟨1, b⟩\} \in E \leftrightarrow y = b)$
139		equcom	$⊢ y = b \leftrightarrow b = y$
140	138 139	bitrdi	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨0, y⟩, ⟨1, b⟩\} \in E \leftrightarrow b = y)$
141	34 140	bitrid	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (\{⟨1, b⟩, ⟨0, y⟩\} \in E \leftrightarrow b = y)$
142	35 36 141	mpanl12	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, b⟩, ⟨0, y⟩\} \in E \leftrightarrow b = y)$
143	142 74	biimtrdi	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to (\{⟨1, b⟩, ⟨0, y⟩\} \in E \to ⟨1, y⟩ = ⟨1, b⟩)$
144	143	adantld	$⊢ (b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
145	144	adantl	$⊢ (K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)$
146	132	adantl	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to \{K, ⟨1, b⟩\} = \{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\}$
147	146	eleq1d	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (\{K, ⟨1, b⟩\} \in E \leftrightarrow \{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E)$
148	49	adantr	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (\{⟨1, b⟩, L\} \in E \leftrightarrow \{⟨1, b⟩, ⟨0, y⟩\} \in E)$
149	147 148	anbi12d	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \leftrightarrow (\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E))$
150	149	imbi1d	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩) \leftrightarrow ((\{⟨1, (y - 2) \mod 5⟩, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, ⟨0, y⟩\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
151	145 150	imbitrrid	$⊢ (L = ⟨0, y⟩ \land K = ⟨1, (y - 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
152	151	ex	$⊢ L = ⟨0, y⟩ \to (K = ⟨1, (y - 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
153		eqeq2	$⊢ ⟨1, (y - 2) \mod 5⟩ = L \to (K = ⟨1, (y - 2) \mod 5⟩ \leftrightarrow K = L)$
154	153	eqcoms	$⊢ L = ⟨1, (y - 2) \mod 5⟩ \to (K = ⟨1, (y - 2) \mod 5⟩ \leftrightarrow K = L)$
155		eqneqall	$⊢ K = L \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
156	155	impd	$⊢ K = L \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
157	154 156	biimtrdi	$⊢ L = ⟨1, (y - 2) \mod 5⟩ \to (K = ⟨1, (y - 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
158	137 152 157	3jaoi	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩) \to (K = ⟨1, (y - 2) \mod 5⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
159	83 114 158	3jaod	$⊢ (L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩) \to ((K = ⟨1, (y + 2) \mod 5⟩ \lor K = ⟨0, y⟩ \lor K = ⟨1, (y - 2) \mod 5⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
160	159	imp	$⊢ ((L = ⟨1, (y + 2) \mod 5⟩ \lor L = ⟨0, y⟩ \lor L = ⟨1, (y - 2) \mod 5⟩) \land (K = ⟨1, (y + 2) \mod 5⟩ \lor K = ⟨0, y⟩ \lor K = ⟨1, (y - 2) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
161	23 160	biimtrdi	$⊢ 2^{nd} (X) = y \to (((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \land (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
162	7 161	syl	$⊢ X = ⟨1, y⟩ \to (((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \land (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
163		eqeq1	$⊢ X = ⟨1, y⟩ \to (X = ⟨1, b⟩ \leftrightarrow ⟨1, y⟩ = ⟨1, b⟩)$
164	163	imbi2d	$⊢ X = ⟨1, y⟩ \to (((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩) \leftrightarrow ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩))$
165	164	imbi2d	$⊢ X = ⟨1, y⟩ \to (((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)) \leftrightarrow ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to ⟨1, y⟩ = ⟨1, b⟩)))$
166	162 165	sylibrd	$⊢ X = ⟨1, y⟩ \to (((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \land (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
167	166	adantl	$⊢ (X \in V \land X = ⟨1, y⟩) \to (((L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \land (K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩)) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
168	167	expdcom	$⊢ (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((K = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor K = ⟨0, 2^{nd} (X)⟩ \lor K = ⟨1, (2^{nd} (X) - 2) \mod 5⟩) \to ((X \in V \land X = ⟨1, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem4

Proof