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

Metamath Proof Explorer

Theorem struct2griedg

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, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

Ref Expression
Hypothesis struct2grvtx.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ }
Assertion struct2griedg ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐺 ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 struct2grvtx.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ }
2 1 struct2grstr ⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , ( .ef ‘ ndx ) ⟩
3 2 a1i ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐺 Struct ⟨ ( Base ‘ ndx ) , ( .ef ‘ ndx ) ⟩ )
4 simpl ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝑉 ∈ 𝑋 )
5 simpr ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → 𝐸 ∈ 𝑌 )
6 1 eqimss2i ⊢ { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺
7 6 a1i ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ , ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ } ⊆ 𝐺 )
8 3 4 5 7 structgrssiedg ⊢ ( ( 𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( iEdg ‘ 𝐺 ) = 𝐸 )