Theorem funiedgdmge2val

Description: The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		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)$$
2		fundmge2nop0	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
3	2	iffalsed	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge 2\le \left|\mathrm{dom}G\right|\right)\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)$$
4	1 3	eqtrid	$$⊢\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)$$