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	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
		structgrssvtx.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
		structgrssvtx.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑍 )
		structgrssvtx.s	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
	Assertion	structgrssiedg	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	⊢ ( 𝜑 → 𝐺 Struct 𝑋 )
2		structgrssvtx.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑌 )
3		structgrssvtx.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑍 )
4		structgrssvtx.s	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
5	1 2 3 4	structgrssvtxlem	⊢ ( 𝜑 → 2 ≤ ( ♯ ‘ dom 𝐺 ) )
6		opex	⊢ ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ V
7		opex	⊢ ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ V
8	6 7	prss	⊢ ( ( ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 ∧ ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 ) ↔ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
9		simpr	⊢ ( ( ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ ∈ 𝐺 ∧ ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 ) → ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 )
10	8 9	sylbir	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 → ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 )
11	4 10	syl	⊢ ( 𝜑 → ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ∈ 𝐺 )
12	1 5 3 11	edgfiedgval	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = 𝐸 )