Theorem usgrexmpl2vtx

Description: The vertices 0 , 1 , 2 , 3 , 4 , 5 of the graph G = <. V , E >. . (Contributed by AV, 3-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	usgrexmpl2vtx	⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 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	3	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
5	1	ovexi	⊢ 𝑉 ∈ V
6		s7cli	⊢ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ∈ Word V
7	2 6	eqeltri	⊢ 𝐸 ∈ Word V
8		opvtxfv	⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ Word V ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9	5 7 8	mp2an	⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉
10	4 9	eqtri	⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11		fz0to5un2tp	⊢ ( 0 ... 5 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
12	10 1 11	3eqtri	⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )