# 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}\in \mathrm{V}$
snstrvtxval.g ${⊢}{G}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}$
Assertion snstriedgval ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{iEdg}\left({G}\right)=\varnothing$

### Proof

Step Hyp Ref Expression
1 snstrvtxval.v ${⊢}{V}\in \mathrm{V}$
2 snstrvtxval.g ${⊢}{G}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}$
3 iedgval ${⊢}\mathrm{iEdg}\left({G}\right)=if\left({G}\in \left(\mathrm{V}×\mathrm{V}\right),{2}^{nd}\left({G}\right),\mathrm{ef}\left({G}\right)\right)$
4 3 a1i ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{iEdg}\left({G}\right)=if\left({G}\in \left(\mathrm{V}×\mathrm{V}\right),{2}^{nd}\left({G}\right),\mathrm{ef}\left({G}\right)\right)$
5 necom ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}↔{\mathrm{Base}}_{\mathrm{ndx}}\ne {V}$
6 fvex ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$
7 6 1 2 funsndifnop ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne {V}\to ¬{G}\in \left(\mathrm{V}×\mathrm{V}\right)$
8 5 7 sylbi ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to ¬{G}\in \left(\mathrm{V}×\mathrm{V}\right)$
9 8 iffalsed ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to if\left({G}\in \left(\mathrm{V}×\mathrm{V}\right),{2}^{nd}\left({G}\right),\mathrm{ef}\left({G}\right)\right)=\mathrm{ef}\left({G}\right)$
10 snex ${⊢}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}\in \mathrm{V}$
11 10 a1i ${⊢}{G}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}\in \mathrm{V}$
12 2 11 eqeltrid ${⊢}{G}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}\to {G}\in \mathrm{V}$
13 edgfndxid ${⊢}{G}\in \mathrm{V}\to \mathrm{ef}\left({G}\right)={G}\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)$
14 2 12 13 mp2b ${⊢}\mathrm{ef}\left({G}\right)={G}\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)$
15 slotsbaseefdif ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$
16 15 nesymi ${⊢}¬\mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$
17 16 a1i ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to ¬\mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$
18 fvex ${⊢}\mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{V}$
19 18 elsn ${⊢}\mathrm{ef}\left(\mathrm{ndx}\right)\in \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}↔\mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$
20 17 19 sylnibr ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to ¬\mathrm{ef}\left(\mathrm{ndx}\right)\in \left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}$
21 2 dmeqi ${⊢}\mathrm{dom}{G}=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}$
22 dmsnopg ${⊢}{V}\in \mathrm{V}\to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}$
23 1 22 mp1i ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},{V}⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}$
24 21 23 syl5eq ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{dom}{G}=\left\{{\mathrm{Base}}_{\mathrm{ndx}}\right\}$
25 20 24 neleqtrrd ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to ¬\mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{dom}{G}$
26 ndmfv ${⊢}¬\mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{dom}{G}\to {G}\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)=\varnothing$
27 25 26 syl ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to {G}\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)=\varnothing$
28 14 27 syl5eq ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{ef}\left({G}\right)=\varnothing$
29 4 9 28 3eqtrd ${⊢}{V}\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{iEdg}\left({G}\right)=\varnothing$