This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrexmpl1

Description: G is a simple graph of six vertices 0 , 1 , 2 , 3 , 4 , 5 , with edges { 0 , 1 } , { 1 , 2 } , { 0 , 2 } , { 0 , 3 } , { 3 , 4 } , { 3 , 5 } , { 4 , 5 } . (Contributed by AV, 3-Aug-2025)

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

Proof

Step Hyp Ref Expression
1 usgrexmpl1.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl1.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩
3 usgrexmpl1.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 1 2 usgrexmpl1lem ⊢ 𝐸 : dom 𝐸 –1-1→ { 𝑒 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑒 ) = 2 }
5 3 eleq1i ⊢ ( 𝐺 ∈ USGraph ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ USGraph )
6 1 ovexi ⊢ 𝑉 ∈ V
7 s7cli ⊢ ⟨“ { 0 , 1 } { 0 , 2 } { 1 , 2 } { 0 , 3 } { 3 , 4 } { 3 , 5 } { 4 , 5 } ”⟩ ∈ 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