Metamath Proof Explorer

Theorem pgnbgreunbgrlem6

Description: Lemma 6 for pgnbgreunbgr . (Contributed by AV, 20-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion pgnbgreunbgrlem6 ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 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 2 nbgrcl ⊢ ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) → 𝑋 ∈ 𝑉 )
6 5 4 eleq2s ⊢ ( 𝐾 ∈ 𝑁 → 𝑋 ∈ 𝑉 )
7 6 3ad2ant1 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → 𝑋 ∈ 𝑉 )
8 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
9 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
10 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
11 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
12 10 11 1 2 gpgvtxel ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 5 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ) )
13 8 9 12 mp2an ⊢ ( 𝑋 ∈ 𝑉 ↔ ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 5 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ )
14 13 biimpi ⊢ ( 𝑋 ∈ 𝑉 → ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 5 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ )
15 14 adantl ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) → ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 5 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ )
16 vex ⊢ 𝑥 ∈ V
17 16 elpr ⊢ ( 𝑥 ∈ { 0 , 1 } ↔ ( 𝑥 = 0 ∨ 𝑥 = 1 ) )
18 8 9 pm3.2i ⊢ ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) )
19 c0ex ⊢ 0 ∈ V
20 vex ⊢ 𝑦 ∈ V
21 19 20 op1std ⊢ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 1st ‘ 𝑋 ) = 0 )
22 21 anim1ci ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) )
23 11 1 2 4 gpgnbgrvtx0 ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ ( 1st ‘ 𝑋 ) = 0 ) ) → 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } )
24 18 22 23 sylancr ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } )
25 eleq2 ⊢ ( 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } → ( 𝐾 ∈ 𝑁 ↔ 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) )
26 eleq2 ⊢ ( 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } → ( 𝐿 ∈ 𝑁 ↔ 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) )
27 25 26 anbi12d ⊢ ( 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ↔ ( 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) ) )
28 27 adantl ⊢ ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ↔ ( 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) ) )
29 eltpi ⊢ ( 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } → ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) )
30 eltpi ⊢ ( 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } → ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) )
31 1 2 3 4 pgnbgreunbgrlem5 ⊢ ( ( 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
32 30 31 syl ⊢ ( 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } → ( ( 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
33 29 32 mpan9 ⊢ ( ( 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
34 33 com12 ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
35 34 adantr ⊢ ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
36 28 35 sylbid ⊢ ( ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑁 = { ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) + 1 ) mod 5 ) ⟩ , ⟨ 1 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 0 , ( ( ( 2nd ‘ 𝑋 ) − 1 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
37 24 36 mpdan ⊢ ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
38 37 com12 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝑋 = ⟨ 0 , 𝑦 ⟩ ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
39 38 expd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( 𝑋 ∈ 𝑉 → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
40 39 com24 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
41 40 expd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) ) )
42 41 3impia ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
43 42 expdimp ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
44 43 com23 ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
45 44 imp31 ⊢ ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
46 opeq1 ⊢ ( 𝑥 = 0 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 0 , 𝑦 ⟩ )
47 46 eqeq2d ⊢ ( 𝑥 = 0 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 0 , 𝑦 ⟩ ) )
48 47 imbi1d ⊢ ( 𝑥 = 0 → ( ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ↔ ( 𝑋 = ⟨ 0 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
49 45 48 imbitrrid ⊢ ( 𝑥 = 0 → ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
50 opeq1 ⊢ ( 𝑥 = 1 → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 1 , 𝑦 ⟩ )
51 50 eqeq2d ⊢ ( 𝑥 = 1 → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) )
52 51 adantr ⊢ ( ( 𝑥 = 1 ∧ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) )
53 2 eleq2i ⊢ ( 𝑋 ∈ 𝑉 ↔ 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
54 53 biimpi ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( Vtx ‘ 𝐺 ) )
55 1ex ⊢ 1 ∈ V
56 55 20 op1std ⊢ ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( 1st ‘ 𝑋 ) = 1 )
57 54 56 anim12i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 1st ‘ 𝑋 ) = 1 ) )
58 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
59 11 1 58 4 gpgnbgrvtx1 ⊢ ( ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) ∧ ( 𝑋 ∈ ( Vtx ‘ 𝐺 ) ∧ ( 1st ‘ 𝑋 ) = 1 ) ) → 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } )
60 18 57 59 sylancr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } )
61 eleq2 ⊢ ( 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } → ( 𝐾 ∈ 𝑁 ↔ 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) )
62 eleq2 ⊢ ( 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } → ( 𝐿 ∈ 𝑁 ↔ 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) )
63 61 62 anbi12d ⊢ ( 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ↔ ( 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) ) )
64 63 adantl ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) ∧ 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ↔ ( 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) ) )
65 eltpi ⊢ ( 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } → ( 𝐾 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ ) )
66 eltpi ⊢ ( 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } → ( 𝐿 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ ) )
67 1 2 3 4 pgnbgreunbgrlem4 ⊢ ( ( 𝐿 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ ∨ 𝐿 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐿 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ ) → ( ( 𝐾 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
68 66 67 syl ⊢ ( 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } → ( ( 𝐾 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ ∨ 𝐾 = ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ ∨ 𝐾 = ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
69 65 68 mpan9 ⊢ ( ( 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
70 69 com12 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
71 70 adantr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) ∧ 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ∧ 𝐿 ∈ { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
72 64 71 sylbid ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) ∧ 𝑁 = { ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) + 2 ) mod 5 ) ⟩ , ⟨ 0 , ( 2nd ‘ 𝑋 ) ⟩ , ⟨ 1 , ( ( ( 2nd ‘ 𝑋 ) − 2 ) mod 5 ) ⟩ } ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
73 60 72 mpdan ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
74 73 com12 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑋 = ⟨ 1 , 𝑦 ⟩ ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
75 74 expd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
76 75 com23 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( 𝑋 ∈ 𝑉 → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
77 76 com24 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( ( 𝐾 ≠ 𝐿 ∧ ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
78 77 expd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( 𝐾 ≠ 𝐿 → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) ) )
79 78 3impia ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ( ( 𝑏 ∈ ( 0 ..^ 5 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
80 79 expdimp ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑋 ∈ 𝑉 → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
81 80 com23 ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 ∈ 𝑉 → ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
82 81 imp31 ⊢ ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
83 82 adantl ⊢ ( ( 𝑥 = 1 ∧ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑋 = ⟨ 1 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
84 52 83 sylbid ⊢ ( ( 𝑥 = 1 ∧ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
85 84 ex ⊢ ( 𝑥 = 1 → ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
86 49 85 jaoi ⊢ ( ( 𝑥 = 0 ∨ 𝑥 = 1 ) → ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
87 17 86 sylbi ⊢ ( 𝑥 ∈ { 0 , 1 } → ( ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
88 87 expd ⊢ ( 𝑥 ∈ { 0 , 1 } → ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
89 88 com12 ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑥 ∈ { 0 , 1 } → ( 𝑦 ∈ ( 0 ..^ 5 ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) ) )
90 89 impd ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑥 ∈ { 0 , 1 } ∧ 𝑦 ∈ ( 0 ..^ 5 ) ) → ( 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) ) )
91 90 rexlimdvv ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ∃ 𝑥 ∈ { 0 , 1 } ∃ 𝑦 ∈ ( 0 ..^ 5 ) 𝑋 = ⟨ 𝑥 , 𝑦 ⟩ → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
92 15 91 mpd ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ∧ 𝑋 ∈ 𝑉 ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
93 7 92 mpidan ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )