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 𝐼 = ( .ef ‘ ndx )
setsvtx.s ( 𝜑𝐺 Struct 𝑋 )
setsvtx.b ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
setsvtx.e ( 𝜑𝐸𝑊 )
Assertion setsiedg ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )

Proof

Step Hyp Ref Expression
1 setsvtx.i 𝐼 = ( .ef ‘ ndx )
2 setsvtx.s ( 𝜑𝐺 Struct 𝑋 )
3 setsvtx.b ( 𝜑 → ( Base ‘ ndx ) ∈ dom 𝐺 )
4 setsvtx.e ( 𝜑𝐸𝑊 )
5 fvexd ( 𝜑 → ( .ef ‘ ndx ) ∈ V )
6 2 5 4 setsn0fun ( 𝜑 → Fun ( ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ∖ { ∅ } ) )
7 2 5 4 3 basprssdmsets ( 𝜑 → { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) )
8 funiedgval ( ( Fun ( ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ∖ { ∅ } ) ∧ { ( Base ‘ ndx ) , ( .ef ‘ ndx ) } ⊆ dom ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) → ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
9 6 7 8 syl2anc ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
10 1 opeq1i 𝐼 , 𝐸 ⟩ = ⟨ ( .ef ‘ ndx ) , 𝐸
11 10 oveq2i ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) = ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ )
12 11 fveq2i ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) )
13 12 a1i ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = ( iEdg ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
14 structex ( 𝐺 Struct 𝑋𝐺 ∈ V )
15 2 14 syl ( 𝜑𝐺 ∈ V )
16 edgfid .ef = Slot ( .ef ‘ ndx )
17 16 setsid ( ( 𝐺 ∈ V ∧ 𝐸𝑊 ) → 𝐸 = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
18 15 4 17 syl2anc ( 𝜑𝐸 = ( .ef ‘ ( 𝐺 sSet ⟨ ( .ef ‘ ndx ) , 𝐸 ⟩ ) ) )
19 9 13 18 3eqtr4d ( 𝜑 → ( iEdg ‘ ( 𝐺 sSet ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )