Metamath Proof Explorer

Theorem pgnbgreunbgrlem3

Description: Lemma 3 for pgnbgreunbgr . (Contributed by AV, 18-Nov-2025)

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