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 } } ) ) } )