pgnbgreunbgrlem3

	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	pgnbgreunbgrlem3	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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		opeq1	$⊢ x = 0 \to ⟨x, y⟩ = ⟨0, y⟩$
19	18	eqeq2d	$⊢ x = 0 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨0, y⟩)$
20	19	adantr	$⊢ (x = 0 \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 = ⟨0, y⟩)$
21	8 9	pm3.2i	$⊢ (5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉))$
22	2	eleq2i	$⊢ X \in V \leftrightarrow X \in Vtx (G)$
23	22	biimpi	$⊢ X \in V \to X \in Vtx (G)$
24		c0ex	$⊢ 0 \in V$
25		vex	$⊢ y \in V$
26	24 25	op1std	$⊢ X = ⟨0, y⟩ \to 1^{st} (X) = 0$
27	23 26	anim12i	$⊢ (X \in V \land X = ⟨0, y⟩) \to (X \in Vtx (G) \land 1^{st} (X) = 0)$
28		eqid	$⊢ Vtx (G) = Vtx (G)$
29	11 1 28 4	gpgnbgrvtx0	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (X \in Vtx (G) \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⟩\}$
30	21 27 29	sylancr	$⊢ (X \in V \land X = ⟨0, y⟩) \to N = \{⟨0, (2^{nd} (X) + 1) \mod 5⟩, ⟨1, 2^{nd} (X)⟩, ⟨0, (2^{nd} (X) - 1) \mod 5⟩\}$
31		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⟩\})$
32		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⟩\})$
33	31 32	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⟩\}))$
34	33	adantl	$⊢ ((X \in V \land X = ⟨0, y⟩) \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⟩\}))$
35		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⟩)$
36		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⟩)$
37	1 2 3 4	pgnbgreunbgrlem1	$⊢ (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 \in V \land X = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
38	36 37	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 \in V \land X = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
39	35 38	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 \in V \land X = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
40	39	com12	$⊢ (X \in V \land X = ⟨0, y⟩) \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
41	40	adantr	$⊢ ((X \in V \land X = ⟨0, y⟩) \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
42	34 41	sylbid	$⊢ ((X \in V \land X = ⟨0, y⟩) \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
43	30 42	mpdan	$⊢ (X \in V \land X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
44	43	com12	$⊢ (K \in N \land L \in N) \to ((X \in V \land X = ⟨0, y⟩) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
45	44	expd	$⊢ (K \in N \land L \in N) \to (X \in V \to (X = ⟨0, y⟩ \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
46	45	com23	$⊢ (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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
47	46	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
48	47	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))))$
49	48	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
50	49	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
51	50	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
52	51	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))$
53	52	adantl	$⊢ (x = 0 \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 = ⟨0, y⟩ \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))$
54	20 53	sylbid	$⊢ (x = 0 \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))$
55	54	ex	$⊢ 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
56		1ex	$⊢ 1 \in V$
57	56 25	op1std	$⊢ X = ⟨1, y⟩ \to 1^{st} (X) = 1$
58	57	anim1ci	$⊢ (X = ⟨1, y⟩ \land X \in V) \to (X \in V \land 1^{st} (X) = 1)$
59	11 1 2 4	gpgnbgrvtx1	$⊢ ((5 \in ℤ_{\geq 3} \land 2 \in (1 ..^⌈\frac{5}{2}⌉)) \land (X \in V \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	21 58 59	sylancr	$⊢ (X = ⟨1, y⟩ \land X \in V) \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 = ⟨1, y⟩ \land X \in V) \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	pgnbgreunbgrlem2	$⊢ (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 = ⟨1, y⟩ \land X \in V) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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 = ⟨1, y⟩ \land X \in V) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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 = ⟨1, y⟩ \land X \in V) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
70	69	com12	$⊢ (X = ⟨1, y⟩ \land X \in V) \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
71	70	adantr	$⊢ ((X = ⟨1, y⟩ \land X \in V) \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
72	64 71	sylbid	$⊢ ((X = ⟨1, y⟩ \land X \in V) \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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
73	60 72	mpdan	$⊢ (X = ⟨1, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
74	73	com12	$⊢ (K \in N \land L \in N) \to ((X = ⟨1, y⟩ \land X \in V) \to ((K \neq L \land (b \in (0 ..^5) \land y \in (0 ..^5))) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
75	74	expd	$⊢ (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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
76	75	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
77	76	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))))$
78	77	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
79	78	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
80	79	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))))$
81	80	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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩))$
82		opeq1	$⊢ x = 1 \to ⟨x, y⟩ = ⟨1, y⟩$
83	82	eqeq2d	$⊢ x = 1 \to (X = ⟨x, y⟩ \leftrightarrow X = ⟨1, y⟩)$
84	83	imbi1d	$⊢ x = 1 \to ((X = ⟨x, y⟩ \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)) \leftrightarrow (X = ⟨1, y⟩ \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
85	81 84	imbitrrid	$⊢ 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)))$
86	55 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, 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, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)$
93	7 92	mpidan	$⊢ ((K \in N \land L \in N \land K \neq L) \land b \in (0 ..^5)) \to ((\{K, ⟨0, b⟩\} \in E \land \{⟨0, b⟩, L\} \in E) \to X = ⟨0, b⟩)$

Metamath Proof Explorer

Theorem pgnbgreunbgrlem3

Proof