Metamath Proof Explorer


Theorem usgrexmpl

Description: G is a simple graph of five vertices 0 , 1 , 2 , 3 , 4 , with edges { 0 , 1 } , { 1 , 2 } , { 2 , 0 } , { 0 , 3 } . (Contributed by Alexander van der Vekens, 15-Aug-2017) (Revised by AV, 21-Oct-2020) (Proof shortened by AV, 7-Aug-2025)

Ref Expression
Hypotheses usgrexmpl.v 𝑉 = ( 0 ... 4 )
usgrexmpl.e 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
usgrexmpl.g 𝐺 = ⟨ 𝑉 , 𝐸
Assertion usgrexmpl 𝐺 ∈ USGraph

Proof

Step Hyp Ref Expression
1 usgrexmpl.v 𝑉 = ( 0 ... 4 )
2 usgrexmpl.e 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
3 usgrexmpl.g 𝐺 = ⟨ 𝑉 , 𝐸
4 1 2 usgrexmplef 𝐸 : dom 𝐸1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
5 3 eleq1i ( 𝐺 ∈ USGraph ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph )
6 1 ovexi 𝑉 ∈ V
7 s4cli ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩ ∈ Word V
8 2 7 eqeltri 𝐸 ∈ Word V
9 isusgrop ( ( 𝑉 ∈ V ∧ 𝐸 ∈ Word V ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ↔ 𝐸 : dom 𝐸1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } ) )
10 6 8 9 mp2an ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph ↔ 𝐸 : dom 𝐸1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
11 5 10 bitri ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 } )
12 4 11 mpbir 𝐺 ∈ USGraph