# 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
`|- ( ph -> G Struct X )`
setsvtx.b
`|- ( ph -> ( Base ` ndx ) e. dom G )`
setsvtx.e
`|- ( ph -> E e. W )`
Assertion setsvtx
`|- ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )`

### Proof

Step Hyp Ref Expression
1 setsvtx.i
` |-  I = ( .ef ` ndx )`
2 setsvtx.s
` |-  ( ph -> G Struct X )`
3 setsvtx.b
` |-  ( ph -> ( Base ` ndx ) e. dom G )`
4 setsvtx.e
` |-  ( ph -> E e. W )`
5 1 fvexi
` |-  I e. _V`
6 5 a1i
` |-  ( ph -> I e. _V )`
7 2 6 4 setsn0fun
` |-  ( ph -> 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
` |-  ( ph -> { ( Base ` ndx ) , I } C_ dom ( G sSet <. I , E >. ) )`
11 9 10 eqsstrid
` |-  ( ph -> { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom ( G sSet <. I , E >. ) )`
12 funvtxval
` |-  ( ( Fun ( ( G sSet <. I , E >. ) \ { (/) } ) /\ { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom ( G sSet <. I , E >. ) ) -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` ( G sSet <. I , E >. ) ) )`
13 7 11 12 syl2anc
` |-  ( ph -> ( 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 eqtr4di
` |-  ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )`