Metamath Proof Explorer


Theorem iedgvalsnop

Description: Degenerated case 2 for edges: The set of indexed edges of a singleton containing an ordered pair with equal components is the singleton containing the component. (Contributed by AV, 24-Sep-2020) (Proof shortened by AV, 15-Jul-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses vtxvalsnop.b
|- B e. _V
vtxvalsnop.g
|- G = { <. B , B >. }
Assertion iedgvalsnop
|- ( iEdg ` G ) = { B }

Proof

Step Hyp Ref Expression
1 vtxvalsnop.b
 |-  B e. _V
2 vtxvalsnop.g
 |-  G = { <. B , B >. }
3 2 fveq2i
 |-  ( iEdg ` G ) = ( iEdg ` { <. B , B >. } )
4 1 snopeqopsnid
 |-  { <. B , B >. } = <. { B } , { B } >.
5 4 fveq2i
 |-  ( iEdg ` { <. B , B >. } ) = ( iEdg ` <. { B } , { B } >. )
6 snex
 |-  { B } e. _V
7 6 6 opiedgfvi
 |-  ( iEdg ` <. { B } , { B } >. ) = { B }
8 3 5 7 3eqtri
 |-  ( iEdg ` G ) = { B }