Metamath Proof Explorer


Theorem 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 V × V 1 st G Base G

Proof

Step Hyp Ref Expression
1 eleq1 g = G g V × V G V × V
2 fveq2 g = G 1 st g = 1 st G
3 fveq2 g = G Base g = Base G
4 1 2 3 ifbieq12d g = G if g V × V 1 st g Base g = if G V × V 1 st G Base G
5 df-vtx Vtx = g V if g V × V 1 st g Base g
6 fvex 1 st G V
7 fvex Base G V
8 6 7 ifex if G V × V 1 st G Base G V
9 4 5 8 fvmpt G V Vtx G = if G V × V 1 st G Base G
10 fvprc ¬ G V Base G =
11 prcnel ¬ G V ¬ G V × V
12 11 iffalsed ¬ G V if G V × V 1 st G Base G = Base G
13 fvprc ¬ G V Vtx G =
14 10 12 13 3eqtr4rd ¬ G V Vtx G = if G V × V 1 st G Base G
15 9 14 pm2.61i Vtx G = if G V × V 1 st G Base G