pgnbgreunbgrlem6

	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	pgnbgreunbgrlem6	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \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	2	nbgrcl	$⊢ K \in (G NeighbVtx X) \to X \in V$
6	5 4	eleq2s	$⊢ K \in N \to X \in V$
7	6	3ad2ant1	$⊢ (K \in N \land L \in N \land K \neq L) \to X \in V$
8		5eluz3	$⊢ 5 \in ℤ_{\geq 3}$
9		pglem	$⊢ 2 \in (1 ..^⌈\frac{5}{2}⌉)$
10		eqid	$⊢ (0 ..^5) = (0 ..^5)$
11		eqid	$⊢ (1 ..^⌈\frac{5}{2}⌉) = (1 ..^⌈\frac{5}{2}⌉)$
12	10 11 1 2	gpgvtxel	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \to (X \in V \leftrightarrow \exists x \in \{0, 1\} \exists y \in (0 ..^5) X = ⟨x, y⟩)$
13	8 9 12	mp2an	$⊢ X \in V \leftrightarrow \exists x \in \{0, 1\} \exists y \in (0 ..^5) X = ⟨x, y⟩$
14	13	biimpi	$⊢ X \in V \to \exists x \in \{0, 1\} \exists y \in (0 ..^5) X = ⟨x, y⟩$
15	14	adantl	$⊢ (((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \to \exists x \in \{0, 1\} \exists y \in (0 ..^5) X = ⟨x, y⟩$
16		vex	$⊢ x \in V$
17	16	elpr	$⊢ x \in \{0, 1\} \leftrightarrow (x = 0 \lor x = 1)$
18	8 9	pm3.2i	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉))$
19		c0ex	$⊢ 0 \in V$
20		vex	$⊢ y \in V$
21	19 20	op1std	$⊢ X = ⟨0, y⟩ \to 1^{st} (X) = 0$
22	21	anim1ci	$⊢ (X = ⟨0, y⟩ \land X \in V) \to (X \in V \land 1^{st} (X) = 0)$
23	11 1 2 4	gpgnbgrvtx0	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (X \in V \land 1^{st} (X) = 0)) \to N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}$
24	18 22 23	sylancr	$⊢ (X = ⟨0, y⟩ \land X \in V) \to N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}$
25		eleq2	$⊢ N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \to (K \in N \leftrightarrow K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\})$
26		eleq2	$⊢ N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \to (L \in N \leftrightarrow L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\})$
27	25 26	anbi12d	$⊢ N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \to ((K \in N \land L \in N) \leftrightarrow (K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \land L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}))$
28	27	adantl	$⊢ ((X = ⟨0, y⟩ \land X \in V) \land N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}) \to ((K \in N \land L \in N) \leftrightarrow (K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \land L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}))$
29		eltpi	$⊢ K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \to (K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)$
30		eltpi	$⊢ L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \to (L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩)$
31	1 2 3 4	pgnbgreunbgrlem5	$⊢ (L = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor L = ⟨1, 2^{nd} (X)⟩ \lor L = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((X = ⟨0, y⟩ \land X \in V) \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⟩))))$
32	30 31	syl	$⊢ L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \to ((K = ⟨0, (2^{nd} (X) + 1) \mod 5⟩ \lor K = ⟨1, 2^{nd} (X)⟩ \lor K = ⟨0, (2^{nd} (X) - 1) \mod 5⟩) \to ((X = ⟨0, y⟩ \land X \in V) \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⟩))))$
33	29 32	mpan9	$⊢ (K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \land L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}) \to ((X = ⟨0, y⟩ \land X \in V) \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⟩)))$
34	33	com12	$⊢ (X = ⟨0, y⟩ \land X \in V) \to ((K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \land L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \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⟩)))$
35	34	adantr	$⊢ ((X = ⟨0, y⟩ \land X \in V) \land N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}) \to ((K \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\} \land L \in \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \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⟩)))$
36	28 35	sylbid	$⊢ ((X = ⟨0, y⟩ \land X \in V) \land N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}) \to ((K \in N \land L \in N) \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⟩)))$
37	24 36	mpdan	$⊢ (X = ⟨0, y⟩ \land X \in V) \to ((K \in N \land L \in N) \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⟩)))$
38	37	com12	$⊢ (K \in N \land L \in N) \to ((X = ⟨0, y⟩ \land X \in V) \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⟩)))$
39	38	expd	$⊢ (K \in N \land L \in N) \to (X = ⟨0, y⟩ \to (X \in V \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⟩))))$
40	39	com24	$⊢ (K \in N \land L \in N) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (X \in V \to (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
41	40	expd	$⊢ (K \in N \land L \in N) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (X \in V \to (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))))$
42	41	3impia	$⊢ (K \in N \land L \in N \land K \neq L) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (X \in V \to (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
43	42	expdimp	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to (y \in (0 ..^5) \to (X \in V \to (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
44	43	com23	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to (X \in V \to (y \in (0 ..^5) \to (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
45	44	imp31	$⊢ ((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5)) \to (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
46		opeq1	$⊢ x = 0 \to ⟨x, y⟩ = ⟨0, y⟩$
47	46	eqeq2d	$⊢ x = 0 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨0, y⟩)$
48	47	imbi1d	$⊢ x = 0 \to ((X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)) \leftrightarrow (X = ⟨0, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
49	45 48	imbitrrid	$⊢ x = 0 \to (((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5)) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
50		opeq1	$⊢ x = 1 \to ⟨x, y⟩ = ⟨1, y⟩$
51	50	eqeq2d	$⊢ x = 1 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
52	51	adantr	$⊢ (x = 1 \land ((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5))) \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
53	2	eleq2i	$⊢ X \in V \leftrightarrow X \in Vtx (G)$
54	53	biimpi	$⊢ X \in V \to X \in Vtx (G)$
55		1ex	$⊢ 1 \in V$
56	55 20	op1std	$⊢ X = ⟨1, y⟩ \to 1^{st} (X) = 1$
57	54 56	anim12i	$⊢ (X \in V \land X = ⟨1, y⟩) \to (X \in Vtx (G) \land 1^{st} (X) = 1)$
58		eqid	$⊢ Vtx (G) = Vtx (G)$
59	11 1 58 4	gpgnbgrvtx1	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (X \in Vtx (G) \land 1^{st} (X) = 1)) \to N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}$
60	18 57 59	sylancr	$⊢ (X \in V \land X = ⟨1, y⟩) \to N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}$
61		eleq2	$⊢ N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \to (K \in N \leftrightarrow K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\})$
62		eleq2	$⊢ N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \to (L \in N \leftrightarrow L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\})$
63	61 62	anbi12d	$⊢ N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \to ((K \in N \land L \in N) \leftrightarrow (K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \land L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}))$
64	63	adantl	$⊢ ((X \in V \land X = ⟨1, y⟩) \land N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}) \to ((K \in N \land L \in N) \leftrightarrow (K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \land L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}))$
65		eltpi	$⊢ K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨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⟩)$
66		eltpi	$⊢ L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \to (L = ⟨1, (2^{nd} (X) + 2) \mod 5⟩ \lor L = ⟨0, 2^{nd} (X)⟩ \lor L = ⟨1, (2^{nd} (X) - 2) \mod 5⟩)$
67	1 2 3 4	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⟩))))$
68	66 67	syl	$⊢ L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨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⟩))))$
69	65 68	mpan9	$⊢ (K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \land L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨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⟩)))$
70	69	com12	$⊢ (X \in V \land X = ⟨1, y⟩) \to ((K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \land L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨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⟩)))$
71	70	adantr	$⊢ ((X \in V \land X = ⟨1, y⟩) \land N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}) \to ((K \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\} \land L \in \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨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⟩)))$
72	64 71	sylbid	$⊢ ((X \in V \land X = ⟨1, y⟩) \land N = \{⟨1, (2^{nd} (X) + 2) \mod 5⟩, ⟨0, 2^{nd} (X)⟩, ⟨1, (2^{nd} (X) - 2) \mod 5⟩\}) \to ((K \in N \land L \in N) \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⟩)))$
73	60 72	mpdan	$⊢ (X \in V \land X = ⟨1, y⟩) \to ((K \in N \land L \in N) \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⟩)))$
74	73	com12	$⊢ (K \in N \land L \in N) \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⟩)))$
75	74	expd	$⊢ (K \in N \land L \in N) \to (X \in V \to (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⟩))))$
76	75	com23	$⊢ (K \in N \land L \in N) \to (X = ⟨1, y⟩ \to (X \in V \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⟩))))$
77	76	com24	$⊢ (K \in N \land L \in N) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to (X \in V \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
78	77	expd	$⊢ (K \in N \land L \in N) \to (K \neq L \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (X \in V \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))))$
79	78	3impia	$⊢ (K \in N \land L \in N \land K \neq L) \to ((b \in (0 ..^5) \land y \in (0 ..^5)) \to (X \in V \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
80	79	expdimp	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to (y \in (0 ..^5) \to (X \in V \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
81	80	com23	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to (X \in V \to (y \in (0 ..^5) \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
82	81	imp31	$⊢ ((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5)) \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
83	82	adantl	$⊢ (x = 1 \land ((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5))) \to (X = ⟨1, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
84	52 83	sylbid	$⊢ (x = 1 \land ((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5))) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
85	84	ex	$⊢ x = 1 \to (((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5)) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
86	49 85	jaoi	$⊢ (x = 0 \lor x = 1) \to (((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5)) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
87	17 86	sylbi	$⊢ x \in \{0, 1\} \to (((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \land y \in (0 ..^5)) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
88	87	expd	$⊢ x \in \{0, 1\} \to ((((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \to (y \in (0 ..^5) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
89	88	com12	$⊢ (((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \to (x \in \{0, 1\} \to (y \in (0 ..^5) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))))$
90	89	impd	$⊢ (((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \to ((x \in \{0, 1\} \land y \in (0 ..^5)) \to (X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)))$
91	90	rexlimdvv	$⊢ (((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \to (\exists x \in \{0, 1\} \exists y \in (0 ..^5) X = ⟨x, y⟩ \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩))$
92	15 91	mpd	$⊢ (((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \land X \in V) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$
93	7 92	mpidan	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to ((\{K, ⟨1, b⟩\} \in E \land \{⟨1, b⟩, L\} \in E) \to X = ⟨1, b⟩)$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem6

Proof