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

Metamath Proof Explorer

Theorem isusgrs

Description: The property of being a simple graph, simplified version of isusgr . (Contributed by Alexander van der Vekens, 13-Aug-2017) (Revised by AV, 13-Oct-2020) (Proof shortened by AV, 24-Nov-2020)

Ref Expression
Hypotheses isuspgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isuspgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isusgrs ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )

Proof

Step Hyp Ref Expression
1 isuspgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isuspgr.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 1 2 isusgr ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
4 prprrab ⊢ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
5 f1eq3 ⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
6 4 5 mp1i ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
7 3 6 bitrd ⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ USGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )