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

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 ⟨ 𝐼 , 𝐸 ⟩ ) ) = 𝐸 )