Metamath Proof Explorer


Theorem setsvtx

Description: The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020) (Revised by AV, 16-Nov-2021)

Ref Expression
Hypotheses setsvtx.i I = ef ndx
setsvtx.s φ G Struct X
setsvtx.b φ Base ndx dom G
setsvtx.e φ E W
Assertion setsvtx φ Vtx G sSet I E = Base G

Proof

Step Hyp Ref Expression
1 setsvtx.i I = ef ndx
2 setsvtx.s φ G Struct X
3 setsvtx.b φ Base ndx dom G
4 setsvtx.e φ E W
5 1 fvexi I V
6 5 a1i φ I V
7 2 6 4 setsn0fun φ Fun G sSet I E
8 1 eqcomi ef ndx = I
9 8 preq2i Base ndx ef ndx = Base ndx I
10 2 6 4 3 basprssdmsets φ Base ndx I dom G sSet I E
11 9 10 eqsstrid φ Base ndx ef ndx dom G sSet I E
12 funvtxval Fun G sSet I E Base ndx ef ndx dom G sSet I E Vtx G sSet I E = Base G sSet I E
13 7 11 12 syl2anc φ Vtx G sSet I E = Base G sSet I E
14 baseid Base = Slot Base ndx
15 slotsbaseefdif Base ndx ef ndx
16 15 1 neeqtrri Base ndx I
17 14 16 setsnid Base G = Base G sSet I E
18 13 17 syl6eqr φ Vtx G sSet I E = Base G