Theorem usgrexmplvtx

Description: The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypotheses	usgrexmpl.v	⊢ 𝑉 = ( 0 ... 4 )
	usgrexmpl.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
	usgrexmpl.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion	usgrexmplvtx	⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl.v	⊢ 𝑉 = ( 0 ... 4 )
2		usgrexmpl.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
3		usgrexmpl.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4	1 2 3	usgrexmpllem	⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 )
5		id	⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( Vtx ‘ 𝐺 ) = 𝑉 )
6		fz0to4untppr	⊢ ( 0 ... 4 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )
7	1 6	eqtri	⊢ 𝑉 = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )
8	5 7	eqtrdi	⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } ) )
9	8	adantr	⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } ) )
10	4 9	ax-mp	⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )