pgnbgreunbgrlem4

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

Proof

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

Metamath Proof Explorer

Theorem pgnbgreunbgrlem4

Proof