This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 basendxnedgfndx ⊢ ( Base ‘ ndx ) ≠ ( .ef ‘ ndx )
16 15 1 neeqtrri ⊢ ( Base ‘ ndx ) ≠ 𝐼
17 14 16 setsnid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) )
18 13 17 eqtr4di ⊢ ( 𝜑 → ( Vtx ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( Base ‘ 𝐺 ) )