Metamath Proof Explorer

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	$⊢ I = ef (ndx)$
		setsvtx.s	$⊢ φ \to G Struct X$
		setsvtx.b	$⊢ φ \to {Base}_{ndx} \in dom G$
		setsvtx.e	$⊢ φ \to E \in W$
	Assertion	setsiedg	$⊢ φ \to iEdg (G sSet ⟨I, E⟩) = E$

Proof

Step	Hyp	Ref	Expression
1		setsvtx.i	$⊢ I = ef (ndx)$
2		setsvtx.s	$⊢ φ \to G Struct X$
3		setsvtx.b	$⊢ φ \to {Base}_{ndx} \in dom G$
4		setsvtx.e	$⊢ φ \to E \in W$
5		fvexd	$⊢ φ \to ef (ndx) \in V$
6	2 5 4	setsn0fun	$⊢ φ \to Fun ((G sSet ⟨ef (ndx), E⟩) ∖ \{\emptyset\})$
7	2 5 4 3	basprssdmsets	$⊢ φ \to \{{Base}_{ndx}, ef (ndx)\} \subseteq dom (G sSet ⟨ef (ndx), E⟩)$
8		funiedgval	$⊢ (Fun ((G sSet ⟨ef (ndx), E⟩) ∖ \{\emptyset\}) \land \{{Base}_{ndx}, ef (ndx)\} \subseteq dom (G sSet ⟨ef (ndx), E⟩)) \to iEdg (G sSet ⟨ef (ndx), E⟩) = ef (G sSet ⟨ef (ndx), E⟩)$
9	6 7 8	syl2anc	$⊢ φ \to iEdg (G sSet ⟨ef (ndx), E⟩) = ef (G sSet ⟨ef (ndx), E⟩)$
10	1	opeq1i	$⊢ ⟨I, E⟩ = ⟨ef (ndx), E⟩$
11	10	oveq2i	$⊢ G sSet ⟨I, E⟩ = G sSet ⟨ef (ndx), E⟩$
12	11	fveq2i	$⊢ iEdg (G sSet ⟨I, E⟩) = iEdg (G sSet ⟨ef (ndx), E⟩)$
13	12	a1i	$⊢ φ \to iEdg (G sSet ⟨I, E⟩) = iEdg (G sSet ⟨ef (ndx), E⟩)$
14		structex	$⊢ G Struct X \to G \in V$
15	2 14	syl	$⊢ φ \to G \in V$
16		edgfid	$⊢ ef = Slot ef (ndx)$
17	16	setsid	$⊢ (G \in V \land E \in W) \to E = ef (G sSet ⟨ef (ndx), E⟩)$
18	15 4 17	syl2anc	$⊢ φ \to E = ef (G sSet ⟨ef (ndx), E⟩)$
19	9 13 18	3eqtr4d	$⊢ φ \to iEdg (G sSet ⟨I, E⟩) = E$