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 ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpl2nblem ( 𝐾 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 𝐾 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
3 usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 1 2 3 usgrexmpl2 ⊢ 𝐺 ∈ USGraph
5 1 2 3 usgrexmpl2vtx ⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
6 5 eqcomi ⊢ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) = ( Vtx ‘ 𝐺 )
7 1 2 3 usgrexmpl2edg ⊢ ( Edg ‘ 𝐺 ) = ( { { 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 ‘ 𝐺 )
9 6 8 nbusgrvtx ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐾 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ) → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 𝐾 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )
10 4 9 mpan ⊢ ( 𝐾 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) → ( 𝐺 NeighbVtx 𝐾 ) = { 𝑛 ∈ ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } ) ∣ { 𝐾 , 𝑛 } ∈ ( { { 0 , 3 } } ∪ ( { { 0 , 1 } , { 1 , 2 } , { 2 , 3 } } ∪ { { 3 , 4 } , { 4 , 5 } , { 0 , 5 } } ) ) } )