Theorem structiedg0val

Description: The set of indexed edges of an extensible structure with a base set and another slot not being the slot for edge functions is empty. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	structvtxvallem.s	$$⊢S\in \mathbb{N}$$
	structvtxvallem.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<S$$
	structvtxvallem.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
Assertion	structiedg0val	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \mathrm{iEdg}\left(G\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	$$⊢S\in \mathbb{N}$$
2		structvtxvallem.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<S$$
3		structvtxvallem.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
4	3 2 1	2strstr1	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},S⟩$$
5		structn0fun	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},S⟩\to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
6	1 2 3	structvtxvallem	$$⊢\left(V\in X\wedge E\in Y\right)\to 2\le \left|\mathrm{dom}G\right|$$
7		funiedgdmge2val	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \mathrm{iEdg}\left(G\right)=\mathrm{ef}\left(G\right)$$
8	5 6 7	syl2an	$$⊢\left(G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},S⟩\wedge \left(V\in X\wedge E\in Y\right)\right)\to \mathrm{iEdg}\left(G\right)=\mathrm{ef}\left(G\right)$$
9	4 8	mpan	$$⊢\left(V\in X\wedge E\in Y\right)\to \mathrm{iEdg}\left(G\right)=\mathrm{ef}\left(G\right)$$
10	9	3adant3	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \mathrm{iEdg}\left(G\right)=\mathrm{ef}\left(G\right)$$
11		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\in \mathrm{V}$$
12	11	a1i	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\in \mathrm{V}$$
13	3 12	eqeltrid	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}\to G\in \mathrm{V}$$
14		edgfndxid	$$⊢G\in \mathrm{V}\to \mathrm{ef}\left(G\right)=G\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)$$
15	3 13 14	mp2b	$$⊢\mathrm{ef}\left(G\right)=G\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)$$
16		slotsbaseefdif	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$$
17	16	nesymi	$$⊢\neg \mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$$
18	17	a1i	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \neg \mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}$$
19		neneq	$$⊢S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\to \neg S=\mathrm{ef}\left(\mathrm{ndx}\right)$$
20		eqcom	$$⊢\mathrm{ef}\left(\mathrm{ndx}\right)=S\leftrightarrow S=\mathrm{ef}\left(\mathrm{ndx}\right)$$
21	19 20	sylnibr	$$⊢S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\to \neg \mathrm{ef}\left(\mathrm{ndx}\right)=S$$
22	21	3ad2ant3	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \neg \mathrm{ef}\left(\mathrm{ndx}\right)=S$$
23		ioran	$$⊢\neg \left(\mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}\vee \mathrm{ef}\left(\mathrm{ndx}\right)=S\right)\leftrightarrow \left(\neg \mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}\wedge \neg \mathrm{ef}\left(\mathrm{ndx}\right)=S\right)$$
24	18 22 23	sylanbrc	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \neg \left(\mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}\vee \mathrm{ef}\left(\mathrm{ndx}\right)=S\right)$$
25		fvex	$$⊢\mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{V}$$
26	25	elpr	$$⊢\mathrm{ef}\left(\mathrm{ndx}\right)\in \left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}\leftrightarrow \left(\mathrm{ef}\left(\mathrm{ndx}\right)={\mathrm{Base}}_{\mathrm{ndx}}\vee \mathrm{ef}\left(\mathrm{ndx}\right)=S\right)$$
27	24 26	sylnibr	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \neg \mathrm{ef}\left(\mathrm{ndx}\right)\in \left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}$$
28	3	dmeqi	$$⊢\mathrm{dom}G=\mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
29		dmpropg	$$⊢\left(V\in X\wedge E\in Y\right)\to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}$$
30	29	3adant3	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \mathrm{dom}\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}$$
31	28 30	syl5eq	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \mathrm{dom}G=\left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}$$
32	27 31	neleqtrrd	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \neg \mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{dom}G$$
33		ndmfv	$$⊢\neg \mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{dom}G\to G\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)=\varnothing$$
34	32 33	syl	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to G\left(\mathrm{ef}\left(\mathrm{ndx}\right)\right)=\varnothing$$
35	15 34	syl5eq	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \mathrm{ef}\left(G\right)=\varnothing$$
36	10 35	eqtrd	$$⊢\left(V\in X\wedge E\in Y\wedge S\ne \mathrm{ef}\left(\mathrm{ndx}\right)\right)\to \mathrm{iEdg}\left(G\right)=\varnothing$$