Metamath Proof Explorer


Theorem snstriedgval

Description: The set of indexed edges of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See iedgvalsnop for the (degenerate) case where V = ( Basendx ) . (Contributed by AV, 24-Sep-2020)

Ref Expression
Hypotheses snstrvtxval.v V V
snstrvtxval.g G = Base ndx V
Assertion snstriedgval V Base ndx iEdg G =

Proof

Step Hyp Ref Expression
1 snstrvtxval.v V V
2 snstrvtxval.g G = Base ndx V
3 iedgval iEdg G = if G V × V 2 nd G ef G
4 3 a1i V Base ndx iEdg G = if G V × V 2 nd G ef G
5 necom V Base ndx Base ndx V
6 fvex Base ndx V
7 6 1 2 funsndifnop Base ndx V ¬ G V × V
8 5 7 sylbi V Base ndx ¬ G V × V
9 8 iffalsed V Base ndx if G V × V 2 nd G ef G = ef G
10 snex Base ndx V V
11 10 a1i G = Base ndx V Base ndx V V
12 2 11 eqeltrid G = Base ndx V G V
13 edgfndxid G V ef G = G ef ndx
14 2 12 13 mp2b ef G = G ef ndx
15 slotsbaseefdif Base ndx ef ndx
16 15 nesymi ¬ ef ndx = Base ndx
17 16 a1i V Base ndx ¬ ef ndx = Base ndx
18 fvex ef ndx V
19 18 elsn ef ndx Base ndx ef ndx = Base ndx
20 17 19 sylnibr V Base ndx ¬ ef ndx Base ndx
21 2 dmeqi dom G = dom Base ndx V
22 dmsnopg V V dom Base ndx V = Base ndx
23 1 22 mp1i V Base ndx dom Base ndx V = Base ndx
24 21 23 syl5eq V Base ndx dom G = Base ndx
25 20 24 neleqtrrd V Base ndx ¬ ef ndx dom G
26 ndmfv ¬ ef ndx dom G G ef ndx =
27 25 26 syl V Base ndx G ef ndx =
28 14 27 syl5eq V Base ndx ef G =
29 4 9 28 3eqtrd V Base ndx iEdg G =