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

Metamath Proof Explorer

Theorem structgrssiedg

Description: The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020) (Proof shortened by AV, 12-Nov-2021)

		Ref	Expression
	Hypotheses	structgrssvtx.g	$⊢ φ \to G Struct X$
		structgrssvtx.v	$⊢ φ \to V \in Y$
		structgrssvtx.e	$⊢ φ \to E \in Z$
		structgrssvtx.s	$⊢ φ \to \{⟨{Base}_{ndx}, V⟩, ⟨ef (ndx), E⟩\} \subseteq G$
	Assertion	structgrssiedg	$⊢ φ \to iEdg (G) = E$

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	$⊢ φ \to G Struct X$
2		structgrssvtx.v	$⊢ φ \to V \in Y$
3		structgrssvtx.e	$⊢ φ \to E \in Z$
4		structgrssvtx.s	$⊢ φ \to \{⟨{Base}_{ndx}, V⟩, ⟨ef (ndx), E⟩\} \subseteq G$
5	1 2 3 4	structgrssvtxlem	$⊢ φ \to 2 \leq \|dom G\|$
6		opex	$⊢ ⟨{Base}_{ndx}, V⟩ \in V$
7		opex	$⊢ ⟨ef (ndx), E⟩ \in V$
8	6 7	prss	$⊢ (⟨{Base}_{ndx}, V⟩ \in G \land ⟨ef (ndx), E⟩ \in G) \leftrightarrow \{⟨{Base}_{ndx}, V⟩, ⟨ef (ndx), E⟩\} \subseteq G$
9		simpr	$⊢ (⟨{Base}_{ndx}, V⟩ \in G \land ⟨ef (ndx), E⟩ \in G) \to ⟨ef (ndx), E⟩ \in G$
10	8 9	sylbir	$⊢ \{⟨{Base}_{ndx}, V⟩, ⟨ef (ndx), E⟩\} \subseteq G \to ⟨ef (ndx), E⟩ \in G$
11	4 10	syl	$⊢ φ \to ⟨ef (ndx), E⟩ \in G$
12	1 5 3 11	edgfiedgval	$⊢ φ \to iEdg (G) = E$