Theorem konigsbergiedg

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

	Ref	Expression
Hypotheses	konigsberg.v	⊢ 𝑉 = ( 0 ... 3 )
	konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
	konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion	konigsbergiedg	⊢ ( iEdg ‘ 𝐺 ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩

Proof

Step	Hyp	Ref	Expression
1		konigsberg.v	⊢ 𝑉 = ( 0 ... 3 )
2		konigsberg.e	⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
3		konigsberg.g	⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4	1 2	opeq12i	⊢ ⟨ 𝑉 , 𝐸 ⟩ = ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩
5	3 4	eqtri	⊢ 𝐺 = ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩
6	5	fveq2i	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩ )
7		ovex	⊢ ( 0 ... 3 ) ∈ V
8		s7cli	⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
9		opiedgfv	⊢ ( ( ( 0 ... 3 ) ∈ V ∧ ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V ) → ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ )
10	7 8 9	mp2an	⊢ ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
11	6 10	eqtri	⊢ ( iEdg ‘ 𝐺 ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩