# 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 𝐼 = ( .ef ‘ ndx )
setsvtx.s ( 𝜑𝐺 Struct 𝑋 )
setsvtx.b ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
setsvtx.e ( 𝜑𝐸𝑊 )
Assertion setsvtx ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ 𝐺 ) )

### Proof

Step Hyp Ref Expression
1 setsvtx.i 𝐼 = ( .ef ‘ ndx )
2 setsvtx.s ( 𝜑𝐺 Struct 𝑋 )
3 setsvtx.b ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
4 setsvtx.e ( 𝜑𝐸𝑊 )
5 1 fvexi 𝐼 ∈ V
6 5 a1i ( 𝜑𝐼 ∈ V )
7 2 6 4 setsn0fun ( 𝜑 → Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) )
8 1 eqcomi ( .ef ‘ ndx ) = 𝐼
9 8 preq2i { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } = { ( Base ‘ ndx ) , 𝐼 }
10 2 6 4 3 basprssdmsets ( 𝜑 → { ( Base ‘ ndx ) , 𝐼 } ⊆ dom ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
11 9 10 eqsstrid ( 𝜑 → { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
12 funvtxval ( ( Fun ( ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) )
13 7 11 12 syl2anc ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) )
14 baseid Base = Slot ( Base ‘ ndx )
15 slotsbaseefdif ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
16 15 1 neeqtrri ( Base ‘ ndx ) ≠ 𝐼
17 14 16 setsnid ( Base ‘ 𝐺 ) = ( Base ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
18 13 17 eqtr4di ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ 𝐺 ) )