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 ‘ 𝐺 ) )