Theorem konigsbergumgr

Description: The Königsberg graph G is a multigraph. (Contributed by AV, 28-Feb-2021) (Revised by AV, 9-Mar-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	konigsbergumgr	⊢ 𝐺 ∈ UMGraph

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 3	konigsbergiedgw	⊢ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
5		opex	⊢ ⟨ 𝑉 , 𝐸 ⟩ ∈ V
6	3 5	eqeltri	⊢ 𝐺 ∈ V
7		s7cli	⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
8	2 7	eqeltri	⊢ 𝐸 ∈ Word V
9	1 2 3	konigsbergvtx	⊢ ( Vtx ‘ 𝐺 ) = ( 0 ... 3 )
10	1 9	eqtr4i	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
11	1 2 3	konigsbergiedg	⊢ ( iEdg ‘ 𝐺 ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
12	2 11	eqtr4i	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
13	10 12	wrdumgr	⊢ ( ( 𝐺 ∈ V ∧ 𝐸 ∈ Word V ) → ( 𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
14	6 8 13	mp2an	⊢ ( 𝐺 ∈ UMGraph ↔ 𝐸 ∈ Word { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
15	4 14	mpbir	⊢ 𝐺 ∈ UMGraph