vtxval

Description: The set of vertices of a graph. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)

		Ref	Expression
	Assertion	vtxval	$⊢ Vtx (G) = if (G \in (V \times V), 1^{st} (G), {Base}_{G})$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ g = G \to (g \in (V \times V) \leftrightarrow G \in (V \times V))$
2		fveq2	$⊢ g = G \to 1^{st} (g) = 1^{st} (G)$
3		fveq2	$⊢ g = G \to {Base}_{g} = {Base}_{G}$
4	1 2 3	ifbieq12d	$⊢ g = G \to if (g \in (V \times V), 1^{st} (g), {Base}_{g}) = if (G \in (V \times V), 1^{st} (G), {Base}_{G})$
5		df-vtx	$⊢ Vtx = (g \in V ⟼ if (g \in (V \times V), 1^{st} (g), {Base}_{g}))$
6		fvex	$⊢ 1^{st} (G) \in V$
7		fvex	$⊢ {Base}_{G} \in V$
8	6 7	ifex	$⊢ if (G \in (V \times V), 1^{st} (G), {Base}_{G}) \in V$
9	4 5 8	fvmpt	$⊢ G \in V \to Vtx (G) = if (G \in (V \times V), 1^{st} (G), {Base}_{G})$
10		fvprc	$⊢ \neg G \in V \to {Base}_{G} = \emptyset$
11		prcnel	$⊢ \neg G \in V \to \neg G \in (V \times V)$
12	11	iffalsed	$⊢ \neg G \in V \to if (G \in (V \times V), 1^{st} (G), {Base}_{G}) = {Base}_{G}$
13		fvprc	$⊢ \neg G \in V \to Vtx (G) = \emptyset$
14	10 12 13	3eqtr4rd	$⊢ \neg G \in V \to Vtx (G) = if (G \in (V \times V), 1^{st} (G), {Base}_{G})$
15	9 14	pm2.61i	$⊢ Vtx (G) = if (G \in (V \times V), 1^{st} (G), {Base}_{G})$

Metamath Proof Explorer