Theorem konigsbergiedg

Description: The indexed edges of the Königsberg graph G . (Contributed by AV, 28-Feb-2021)

	Ref	Expression
Hypotheses	konigsberg.v	$$⊢V=\left(0\dots 3\right)$$
	konigsberg.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
	konigsberg.g	$$⊢G=⟨V,E⟩$$
Assertion	konigsbergiedg	$$⊢\mathrm{iEdg}\left(G\right)=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$

Proof

Step	Hyp	Ref	Expression
1		konigsberg.v	$$⊢V=\left(0\dots 3\right)$$
2		konigsberg.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
3		konigsberg.g	$$⊢G=⟨V,E⟩$$
4	1 2	opeq12i	$$⊢⟨V,E⟩=⟨\left(0\dots 3\right),⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩⟩$$
5	3 4	eqtri	$$⊢G=⟨\left(0\dots 3\right),⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩⟩$$
6	5	fveq2i	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(⟨\left(0\dots 3\right),⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩⟩\right)$$
7		ovex	$$⊢\left(0\dots 3\right)\in \mathrm{V}$$
8		s7cli	$$⊢⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
9		opiedgfv	$$⊢\left(\left(0\dots 3\right)\in \mathrm{V}\wedge ⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩\in \mathrm{Word}\mathrm{V}\right)\to \mathrm{iEdg}\left(⟨\left(0\dots 3\right),⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩⟩\right)=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
10	7 8 9	mp2an	$$⊢\mathrm{iEdg}\left(⟨\left(0\dots 3\right),⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩⟩\right)=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$
11	6 10	eqtri	$$⊢\mathrm{iEdg}\left(G\right)=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{0,3\right\}\left\{1,2\right\}\left\{1,2\right\}\left\{2,3\right\}\left\{2,3\right\}”⟩$$