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

Metamath Proof Explorer

Theorem isumgrs

Description: The simplified property of being an undirected multigraph. (Contributed by AV, 24-Nov-2020)

Ref Expression
Hypotheses isumgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isumgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isumgrs ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )

Proof

Step Hyp Ref Expression
1 isumgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isumgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 isumgr ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
4 prprrab ⊢ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
5 4 a1i ⊢ ( 𝐺 ∈ 𝑈 → { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 5 feq3d ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
7 3 6 bitrd ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UMGraph ↔ 𝐸 : dom 𝐸 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )