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	|- V = ( 0 ... 4 )
	usgrexmpl.e	|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
	usgrexmpl.g	|- G = <. V , E >.
Assertion	usgrexmplvtx	|- ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl.v	|- V = ( 0 ... 4 )
2		usgrexmpl.e	|- E = <" { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ">
3		usgrexmpl.g	|- G = <. V , E >.
4	1 2 3	usgrexmpllem	|- ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E )
5		id	|- ( ( Vtx ` G ) = V -> ( Vtx ` G ) = V )
6		fz0to4untppr	|- ( 0 ... 4 ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )
7	1 6	eqtri	|- V = ( { 0 , 1 , 2 } u. { 3 , 4 } )
8	5 7	eqtrdi	|- ( ( Vtx ` G ) = V -> ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } ) )
9	8	adantr	|- ( ( ( Vtx ` G ) = V /\ ( iEdg ` G ) = E ) -> ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } ) )
10	4 9	ax-mp	|- ( Vtx ` G ) = ( { 0 , 1 , 2 } u. { 3 , 4 } )