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 } ) )