Theorem setsiedg

Description: The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021) (Revised by AV, 16-Nov-2021)

	Ref	Expression
Hypotheses	setsvtx.i	⊢ 𝐼 = ( .ef ‘ ndx )
	setsvtx.s	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
	setsvtx.b	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
	setsvtx.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
Assertion	setsiedg	⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		setsvtx.i	⊢ 𝐼 = ( .ef ‘ ndx )
2		setsvtx.s	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
3		setsvtx.b	⊢ ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
4		setsvtx.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
5		fvexd	⊢ ( 𝜑 → ( .ef ‘ ndx ) ∈ V )
6	2 5 4	setsn0fun	⊢ ( 𝜑 → Fun ( ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ∖ { ∅ } ) )
7	2 5 4 3	basprssdmsets	⊢ ( 𝜑 → { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) )
8		funiedgval	⊢ ( ( Fun ( ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) → ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
9	6 7 8	syl2anc	⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
10	1	opeq1i	⊢ ⟨ 𝐼 , 𝐸 ⟩ = ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩
11	10	oveq2i	⊢ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ )
12	11	fveq2i	⊢ ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) )
13	12	a1i	⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
14		structex	⊢ ( 𝐺 Struct 𝑋 → 𝐺 ∈ V )
15	2 14	syl	⊢ ( 𝜑 → 𝐺 ∈ V )
16		edgfid	⊢ .ef = Slot ( .ef ‘ ndx )
17	16	setsid	⊢ ( ( 𝐺 ∈ V ∧ 𝐸 ∈ 𝑊 ) → 𝐸 = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
18	15 4 17	syl2anc	⊢ ( 𝜑 → 𝐸 = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
19	9 13 18	3eqtr4d	⊢ ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )