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 ‘ 𝐺 ) = 𝐸 )