Metamath Proof Explorer

Theorem pgnbgreunbgr

Description: In a Petersen graph, two different neighbors of a vertex have exactly one common neighbor, which is the vertex itself. (Contributed by AV, 9-Nov-2025)

Ref Expression
Hypotheses pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
Assertion pgnbgreunbgr ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ∃! 𝑥 ∈ 𝑉 { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 )

Proof

Step Hyp Ref Expression
1 pgnbgreunbgr.g ⊢ 𝐺 = ( 5 gPetersenGr 2 )
2 pgnbgreunbgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 pgnbgreunbgr.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 pgnbgreunbgr.n ⊢ 𝑁 = ( 𝐺 NeighbVtx 𝑋 )
5 preq2 ⊢ ( 𝑥 = 𝑋 → { 𝐾 , 𝑥 } = { 𝐾 , 𝑋 } )
6 preq1 ⊢ ( 𝑥 = 𝑋 → { 𝑥 , 𝐿 } = { 𝑋 , 𝐿 } )
7 5 6 preq12d ⊢ ( 𝑥 = 𝑋 → { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } = { { 𝐾 , 𝑋 } , { 𝑋 , 𝐿 } } )
8 7 sseq1d ⊢ ( 𝑥 = 𝑋 → ( { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 ↔ { { 𝐾 , 𝑋 } , { 𝑋 , 𝐿 } } ⊆ 𝐸 ) )
9 eqeq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝑦 ↔ 𝑋 = 𝑦 ) )
10 9 imbi2d ⊢ ( 𝑥 = 𝑋 → ( ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑥 = 𝑦 ) ↔ ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑋 = 𝑦 ) ) )
11 10 ralbidv ⊢ ( 𝑥 = 𝑋 → ( ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑥 = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑋 = 𝑦 ) ) )
12 8 11 anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 ∧ ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑥 = 𝑦 ) ) ↔ ( { { 𝐾 , 𝑋 } , { 𝑋 , 𝐿 } } ⊆ 𝐸 ∧ ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑋 = 𝑦 ) ) ) )
13 4 eleq2i ⊢ ( 𝐾 ∈ 𝑁 ↔ 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
14 13 biimpi ⊢ ( 𝐾 ∈ 𝑁 → 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
15 14 3ad2ant1 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
16 pgjsgr ⊢ ( 5 gPetersenGr 2 ) ∈ USGraph
17 1 16 eqeltri ⊢ 𝐺 ∈ USGraph
18 3 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ { 𝐾 , 𝑋 } ∈ 𝐸 ) )
19 17 18 ax-mp ⊢ ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ { 𝐾 , 𝑋 } ∈ 𝐸 )
20 15 19 sylib ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → { 𝐾 , 𝑋 } ∈ 𝐸 )
21 usgrumgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UMGraph )
22 17 21 ax-mp ⊢ 𝐺 ∈ UMGraph
23 20 22 jctil ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ( 𝐺 ∈ UMGraph ∧ { 𝐾 , 𝑋 } ∈ 𝐸 ) )
24 2 3 umgrpredgv ⊢ ( ( 𝐺 ∈ UMGraph ∧ { 𝐾 , 𝑋 } ∈ 𝐸 ) → ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
25 simpr ⊢ ( ( 𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
26 23 24 25 3syl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → 𝑋 ∈ 𝑉 )
27 4 eleq2i ⊢ ( 𝐿 ∈ 𝑁 ↔ 𝐿 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
28 13 27 anbi12i ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) ↔ ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ 𝐿 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) )
29 3 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝐿 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ { 𝐿 , 𝑋 } ∈ 𝐸 ) )
30 prcom ⊢ { 𝐿 , 𝑋 } = { 𝑋 , 𝐿 }
31 30 eleq1i ⊢ ( { 𝐿 , 𝑋 } ∈ 𝐸 ↔ { 𝑋 , 𝐿 } ∈ 𝐸 )
32 29 31 bitrdi ⊢ ( 𝐺 ∈ USGraph → ( 𝐿 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ { 𝑋 , 𝐿 } ∈ 𝐸 ) )
33 18 32 anbi12d ⊢ ( 𝐺 ∈ USGraph → ( ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ 𝐿 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( { 𝐾 , 𝑋 } ∈ 𝐸 ∧ { 𝑋 , 𝐿 } ∈ 𝐸 ) ) )
34 17 33 ax-mp ⊢ ( ( 𝐾 ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ 𝐿 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( { 𝐾 , 𝑋 } ∈ 𝐸 ∧ { 𝑋 , 𝐿 } ∈ 𝐸 ) )
35 28 34 sylbb ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ) → ( { 𝐾 , 𝑋 } ∈ 𝐸 ∧ { 𝑋 , 𝐿 } ∈ 𝐸 ) )
36 35 3adant3 ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ( { 𝐾 , 𝑋 } ∈ 𝐸 ∧ { 𝑋 , 𝐿 } ∈ 𝐸 ) )
37 prssi ⊢ ( ( { 𝐾 , 𝑋 } ∈ 𝐸 ∧ { 𝑋 , 𝐿 } ∈ 𝐸 ) → { { 𝐾 , 𝑋 } , { 𝑋 , 𝐿 } } ⊆ 𝐸 )
38 36 37 syl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → { { 𝐾 , 𝑋 } , { 𝑋 , 𝐿 } } ⊆ 𝐸 )
39 prex ⊢ { 𝐾 , 𝑦 } ∈ V
40 prex ⊢ { 𝑦 , 𝐿 } ∈ V
41 39 40 prss ⊢ ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) ↔ { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 )
42 5eluz3 ⊢ 5 ∈ ( ℤ≥ ‘ 3 )
43 pglem ⊢ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
44 eqid ⊢ ( 0 ..^ 5 ) = ( 0 ..^ 5 )
45 eqid ⊢ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) = ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) )
46 44 45 1 2 gpgvtxel ⊢ ( ( 5 ∈ ( ℤ≥ ‘ 3 ) ∧ 2 ∈ ( 1 ..^ ( ⌈ ‘ ( 5 / 2 ) ) ) ) → ( 𝑦 ∈ 𝑉 ↔ ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 5 ) 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ ) )
47 42 43 46 mp2an ⊢ ( 𝑦 ∈ 𝑉 ↔ ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 5 ) 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ )
48 47 biimpi ⊢ ( 𝑦 ∈ 𝑉 → ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 5 ) 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ )
49 48 adantl ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 5 ) 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ )
50 opeq1 ⊢ ( 𝑎 = 0 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 0 , 𝑏 ⟩ )
51 50 eqeq2d ⊢ ( 𝑎 = 0 → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑦 = ⟨ 0 , 𝑏 ⟩ ) )
52 51 adantr ⊢ ( ( 𝑎 = 0 ∧ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑦 = ⟨ 0 , 𝑏 ⟩ ) )
53 1 2 3 4 pgnbgreunbgrlem3 ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) )
54 53 adantlr ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) )
55 preq2 ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → { 𝐾 , 𝑦 } = { 𝐾 , ⟨ 0 , 𝑏 ⟩ } )
56 55 eleq1d ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( { 𝐾 , 𝑦 } ∈ 𝐸 ↔ { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ) )
57 preq1 ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → { 𝑦 , 𝐿 } = { ⟨ 0 , 𝑏 ⟩ , 𝐿 } )
58 57 eleq1d ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( { 𝑦 , 𝐿 } ∈ 𝐸 ↔ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) )
59 56 58 anbi12d ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) ↔ ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ) )
60 eqeq2 ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( 𝑋 = 𝑦 ↔ 𝑋 = ⟨ 0 , 𝑏 ⟩ ) )
61 59 60 imbi12d ⊢ ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ↔ ( ( { 𝐾 , ⟨ 0 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 0 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 0 , 𝑏 ⟩ ) ) )
62 54 61 syl5ibrcom ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) )
63 62 adantl ⊢ ( ( 𝑎 = 0 ∧ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑦 = ⟨ 0 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) )
64 52 63 sylbid ⊢ ( ( 𝑎 = 0 ∧ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) )
65 64 ex ⊢ ( 𝑎 = 0 → ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) )
66 1 2 3 4 pgnbgreunbgrlem6 ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
67 66 adantlr ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
68 preq2 ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → { 𝐾 , 𝑦 } = { 𝐾 , ⟨ 1 , 𝑏 ⟩ } )
69 68 eleq1d ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( { 𝐾 , 𝑦 } ∈ 𝐸 ↔ { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ) )
70 preq1 ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → { 𝑦 , 𝐿 } = { ⟨ 1 , 𝑏 ⟩ , 𝐿 } )
71 70 eleq1d ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( { 𝑦 , 𝐿 } ∈ 𝐸 ↔ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) )
72 69 71 anbi12d ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) ↔ ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) ) )
73 eqeq2 ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( 𝑋 = 𝑦 ↔ 𝑋 = ⟨ 1 , 𝑏 ⟩ ) )
74 72 73 imbi12d ⊢ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ↔ ( ( { 𝐾 , ⟨ 1 , 𝑏 ⟩ } ∈ 𝐸 ∧ { ⟨ 1 , 𝑏 ⟩ , 𝐿 } ∈ 𝐸 ) → 𝑋 = ⟨ 1 , 𝑏 ⟩ ) ) )
75 67 74 syl5ibrcom ⊢ ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) )
76 opeq1 ⊢ ( 𝑎 = 1 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 1 , 𝑏 ⟩ )
77 76 eqeq2d ⊢ ( 𝑎 = 1 → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ ↔ 𝑦 = ⟨ 1 , 𝑏 ⟩ ) )
78 77 imbi1d ⊢ ( 𝑎 = 1 → ( ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ↔ ( 𝑦 = ⟨ 1 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) )
79 75 78 imbitrrid ⊢ ( 𝑎 = 1 → ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) )
80 65 79 jaoi ⊢ ( ( 𝑎 = 0 ∨ 𝑎 = 1 ) → ( ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) )
81 80 expd ⊢ ( ( 𝑎 = 0 ∨ 𝑎 = 1 ) → ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑏 ∈ ( 0 ..^ 5 ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) ) )
82 elpri ⊢ ( 𝑎 ∈ { 0 , 1 } → ( 𝑎 = 0 ∨ 𝑎 = 1 ) )
83 81 82 syl11 ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ( 𝑎 ∈ { 0 , 1 } → ( 𝑏 ∈ ( 0 ..^ 5 ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) ) )
84 83 impd ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑎 ∈ { 0 , 1 } ∧ 𝑏 ∈ ( 0 ..^ 5 ) ) → ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) ) )
85 84 rexlimdvv ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ( ∃ 𝑎 ∈ { 0 , 1 } ∃ 𝑏 ∈ ( 0 ..^ 5 ) 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) ) )
86 49 85 mpd ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ( ( { 𝐾 , 𝑦 } ∈ 𝐸 ∧ { 𝑦 , 𝐿 } ∈ 𝐸 ) → 𝑋 = 𝑦 ) )
87 41 86 biimtrrid ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) ∧ 𝑦 ∈ 𝑉 ) → ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑋 = 𝑦 ) )
88 87 ralrimiva ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑋 = 𝑦 ) )
89 38 88 jca ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ( { { 𝐾 , 𝑋 } , { 𝑋 , 𝐿 } } ⊆ 𝐸 ∧ ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑋 = 𝑦 ) ) )
90 12 26 89 rspcedvdw ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ∃ 𝑥 ∈ 𝑉 ( { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 ∧ ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑥 = 𝑦 ) ) )
91 preq2 ⊢ ( 𝑥 = 𝑦 → { 𝐾 , 𝑥 } = { 𝐾 , 𝑦 } )
92 preq1 ⊢ ( 𝑥 = 𝑦 → { 𝑥 , 𝐿 } = { 𝑦 , 𝐿 } )
93 91 92 preq12d ⊢ ( 𝑥 = 𝑦 → { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } = { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } )
94 93 sseq1d ⊢ ( 𝑥 = 𝑦 → ( { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 ↔ { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 ) )
95 94 reu8 ⊢ ( ∃! 𝑥 ∈ 𝑉 { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 ↔ ∃ 𝑥 ∈ 𝑉 ( { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 ∧ ∀ 𝑦 ∈ 𝑉 ( { { 𝐾 , 𝑦 } , { 𝑦 , 𝐿 } } ⊆ 𝐸 → 𝑥 = 𝑦 ) ) )
96 90 95 sylibr ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝐿 ∈ 𝑁 ∧ 𝐾 ≠ 𝐿 ) → ∃! 𝑥 ∈ 𝑉 { { 𝐾 , 𝑥 } , { 𝑥 , 𝐿 } } ⊆ 𝐸 )