pgnbgreunbgrlem1

	Ref	Expression
Hypotheses	pgnbgreunbgr.g	⊢ 𝐺 = ( 5 gPetersenGr 2 )
	pgnbgreunbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	pgnbgreunbgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
	pgnbgreunbgr.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion	pgnbgreunbgrlem1	⊢ ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		pgnbgreunbgr.g	⊢ 𝐺 = ( 5 gPetersenGr 2 )
2		pgnbgreunbgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3		pgnbgreunbgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
4		pgnbgreunbgr.n	⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
5		c0ex	⊢ 0 ∈ V
6		vex	⊢ 𝑦 ∈ V
7	5 6	op2ndd	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 2^nd ‘ 𝑋 ) = 𝑦 )
8		oveq1	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 2^nd ‘ 𝑋 ) + 1 ) = ( 𝑦 + 1 ) )
9	8	oveq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) = ( ( 𝑦 + 1 ) mod 5 ) )
10	9	opeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
11	10	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ↔ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
12		opeq2	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
13	12	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ↔ 𝐿 = ⟨ 1 , 𝑦 ⟩ ) )
14		oveq1	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 2^nd ‘ 𝑋 ) − 1 ) = ( 𝑦 − 1 ) )
15	14	oveq1d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) = ( ( 𝑦 − 1 ) mod 5 ) )
16	15	opeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
17	16	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ↔ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) )
18	11 13 17	3orbi123d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ↔ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) )
19	10	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ↔ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
20	12	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ↔ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) )
21	16	eqeq2d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ↔ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) )
22	19 20 21	3orbi123d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ↔ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) )
23	18 22	anbi12d	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) ↔ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) ) )
24		simpr	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
25		simpl	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
26	24 25	neeq12d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
27		eqid	⊢ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩
28		eqneqall	⊢ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
29	27 28	ax-mp	⊢ ( ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
30	26 29	biimtrdi	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
31	30	impd	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
32	31	ex	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
33		5eluz3	⊢ 5 ∈ ( ℤ_≥ ‘ 3 )
34		pglem	⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
35		eqid	⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
36		eqid	⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
37	35 36 1 3	gpgedgiov	⊢ ( ( ( 5 ∈ ( ℤ_≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ↔ 𝑏 = 𝑦 ) )
38	33 34 37	mpanl12	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ↔ 𝑏 = 𝑦 ) )
39		opeq2	⊢ ( 𝑦 = 𝑏 → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ )
40	39	eqcoms	⊢ ( 𝑏 = 𝑦 → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ )
41	38 40	biimtrdi	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
42	41	adantld	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
43		preq1	⊢ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } )
44	43	eleq1d	⊢ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
45		preq2	⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → { ⟨ 0 , 𝑏 ⟩ , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } )
46	45	eleq1d	⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) )
47	44 46	bi2anan9r	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) ) )
48	47	imbi1d	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
49	42 48	imbitrrid	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
50	49	adantld	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
51	50	ex	⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
52		prcom	⊢ { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ }
53	52	eleq1i	⊢ ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 )
54		prcom	⊢ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } = { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ }
55	54	eleq1i	⊢ ( { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 )
56	53 55	anbi12ci	⊢ ( ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
57		5nn	⊢ 5 ∈ ℕ
58	57	nnzi	⊢ 5 ∈ ℤ
59		uzid	⊢ ( 5 ∈ ℤ → 5 ∈ ( ℤ_≥ ‘ 5 ) )
60	58 59	ax-mp	⊢ 5 ∈ ( ℤ_≥ ‘ 5 )
61	35 36 1 3	gpgedg2ov	⊢ ( ( ( 5 ∈ ( ℤ_≥ ‘ 5 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ↔ 𝑏 = 𝑦 ) )
62	60 34 61	mpanl12	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ↔ 𝑏 = 𝑦 ) )
63		equcomiv	⊢ ( 𝑏 = 𝑦 → 𝑦 = 𝑏 )
64	63	opeq2d	⊢ ( 𝑏 = 𝑦 → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ )
65	62 64	biimtrdi	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
66	56 65	biimtrid	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
67		preq2	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → { ⟨ 0 , 𝑏 ⟩ , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } )
68	67	eleq1d	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
69	44 68	bi2anan9r	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
70	69	imbi1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
71	66 70	imbitrrid	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
72	71	adantld	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
73	72	ex	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
74	32 51 73	3jaoi	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
75		prcom	⊢ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ }
76	75	eleq1i	⊢ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 )
77	76 41	biimtrid	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
78	77	adantrd	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
79		preq1	⊢ ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } )
80	79	eleq1d	⊢ ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
81		preq2	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → { ⟨ 0 , 𝑏 ⟩ , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } )
82	81	eleq1d	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
83	80 82	bi2anan9r	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
84	83	imbi1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
85	78 84	imbitrrid	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
86	85	adantld	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
87	86	ex	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
88		simpr	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → 𝐾 = ⟨ 1 , 𝑦 ⟩ )
89		simpl	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → 𝐿 = ⟨ 1 , 𝑦 ⟩ )
90	88 89	neeq12d	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 1 , 𝑦 ⟩ ≠ ⟨ 1 , 𝑦 ⟩ ) )
91		eqid	⊢ ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩
92		eqneqall	⊢ ( ⟨ 1 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩ → ( ⟨ 1 , 𝑦 ⟩ ≠ ⟨ 1 , 𝑦 ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
93	91 92	ax-mp	⊢ ( ⟨ 1 , 𝑦 ⟩ ≠ ⟨ 1 , 𝑦 ⟩ → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
94	90 93	biimtrdi	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
95	94	impd	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
96	95	ex	⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
97	77	adantrd	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
98	79	adantl	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } )
99	98	eleq1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
100	67	adantr	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → { ⟨ 0 , 𝑏 ⟩ , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } )
101	100	eleq1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) )
102	99 101	anbi12d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
103	102	imbi1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { ⟨ 1 , 𝑦 ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
104	97 103	imbitrrid	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
105	104	adantld	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
106	105	ex	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
107	87 96 106	3jaoi	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( 𝐾 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
108	62 40	biimtrdi	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
109	108	adantl	⊢ ( ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
110	109	a1i	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
111		simpl	⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ )
112		simpr	⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ )
113	111 112	neeq12d	⊢ ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ∧ 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
114	113	ancoms	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( 𝐾 ≠ 𝐿 ↔ ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ) )
115	114	anbi1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ↔ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ≠ ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) ) )
116		preq1	⊢ ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } )
117	116	eleq1d	⊢ ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
118	117 82	bi2anan9r	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) ) )
119	118	imbi1d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
120	110 115 119	3imtr4d	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
121	120	ex	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
122	41	adantld	⊢ ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
123	122	adantl	⊢ ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
124	116	adantl	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → { 𝐾 , ⟨ 0 , 𝑏 ⟩ } = { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } )
125	124	eleq1d	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ↔ { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
126	46	adantr	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) )
127	125 126	anbi12d	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ↔ ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) ) )
128	127	imbi1d	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , ⟨ 1 , 𝑦 ⟩ } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
129	123 128	imbitrrid	⊢ ( ( 𝐿 = ⟨ 1 , 𝑦 ⟩ ∧ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
130	129	ex	⊢ ( 𝐿 = ⟨ 1 , 𝑦 ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
131		eqeq2	⊢ ( ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ = 𝐿 → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ↔ 𝐾 = 𝐿 ) )
132	131	eqcoms	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ↔ 𝐾 = 𝐿 ) )
133		eqneqall	⊢ ( 𝐾 = 𝐿 → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
134	133	impd	⊢ ( 𝐾 = 𝐿 → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
135	132 134	biimtrdi	⊢ ( 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
136	121 130 135	3jaoi	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
137	74 107 136	3jaod	⊢ ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
138	137	imp	⊢ ( ( ( 𝐿 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐿 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( 𝑦 + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , 𝑦 ⟩ ∨ 𝐾 = ⟨ 0 , ( ( 𝑦 − 1 ) mod 5 ) ⟩ ) ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
139	23 138	biimtrdi	⊢ ( ( 2^nd ‘ 𝑋 ) = 𝑦 → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
140	7 139	syl	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
141		eqeq1	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 𝑋 = ⟨ 0 , 𝑏 ⟩ ↔ ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) )
142	141	imbi2d	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ↔ ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) )
143	142	imbi2d	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ) ↔ ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → ⟨ 0 , 𝑦 ⟩ = ⟨ 0 , 𝑏 ⟩ ) ) ) )
144	140 143	sylibrd	⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ) ) )
145	144	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) → ( ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ∧ ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ) ) )
146	145	expdcom	⊢ ( ( 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2^nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2^nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ) ) ) )

Metamath Proof Explorer

Theorem pgnbgreunbgrlem1

Proof