Theorem vtxval0

Description: Degenerated case 1 for vertices: The set of vertices of the empty set is the empty set. (Contributed by AV, 24-Sep-2020)

	Ref	Expression
Assertion	vtxval0	$$⊢\mathrm{Vtx}\left(\varnothing \right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0nelxp	$$⊢\neg \varnothing \in \left(\mathrm{V}\times \mathrm{V}\right)$$
2	1	iffalsei	$$⊢if\left(\varnothing \in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(\varnothing \right),{\mathrm{Base}}_{\varnothing }\right)={\mathrm{Base}}_{\varnothing }$$
3		vtxval	$$⊢\mathrm{Vtx}\left(\varnothing \right)=if\left(\varnothing \in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(\varnothing \right),{\mathrm{Base}}_{\varnothing }\right)$$
4		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
5	2 3 4	3eqtr4i	$$⊢\mathrm{Vtx}\left(\varnothing \right)=\varnothing$$