This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrexmpl2nblem

Description: Lemma for usgrexmpl2nb0 etc. (Contributed by AV, 9-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ V = 0 … 5
usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
usgrexmpl2.g ⊢ G = V E
Assertion usgrexmpl2nblem ⊢ K ∈ 0 1 2 ∪ 3 4 5 → G NeighbVtx K = n ∈ 0 1 2 ∪ 3 4 5 | K n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ V = 0 … 5
2 usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
3 usgrexmpl2.g ⊢ G = V E
4 1 2 3 usgrexmpl2 ⊢ G ∈ USGraph
5 1 2 3 usgrexmpl2vtx ⊢ Vtx ⁡ G = 0 1 2 ∪ 3 4 5
6 5 eqcomi ⊢ 0 1 2 ∪ 3 4 5 = Vtx ⁡ G
7 1 2 3 usgrexmpl2edg ⊢ Edg ⁡ G = 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
8 7 eqcomi ⊢ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5 = Edg ⁡ G
9 6 8 nbusgrvtx ⊢ G ∈ USGraph ∧ K ∈ 0 1 2 ∪ 3 4 5 → G NeighbVtx K = n ∈ 0 1 2 ∪ 3 4 5 | K n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5
10 4 9 mpan ⊢ K ∈ 0 1 2 ∪ 3 4 5 → G NeighbVtx K = n ∈ 0 1 2 ∪ 3 4 5 | K n ∈ 0 3 ∪ 0 1 1 2 2 3 ∪ 3 4 4 5 0 5