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}\times \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}\times \mathrm{V}\right),2^{nd}\left(G\right),\mathrm{ef}\left(G\right)\right)$$
5		necom	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\leftrightarrow {\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 \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
8	5 7	sylbi	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
9	8	iffalsed	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to if\left(G\in \left(\mathrm{V}\times \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	$$⊢\neg \mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$$
17	16	a1i	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \neg \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\}\leftrightarrow \mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$$
20	17 19	sylnibr	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \neg \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 \neg \mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{dom}G$$
26		ndmfv	$$⊢\neg \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$$