Theorem isuspgrop

Description: The property of being an undirected simple pseudograph represented as an ordered pair. The representation as an ordered pair is the usual representation of a graph, see section I.1 of Bollobas p. 1. (Contributed by AV, 25-Nov-2021)

	Ref	Expression
Assertion	isuspgrop	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USPGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 𝑉 , 𝐸 ⟩ ∈ V
2		eqid	⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
3		eqid	⊢ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ )
4	2 3	isuspgr	⊢ ( ⟨ 𝑉 , 𝐸 ⟩ ∈ V → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USPGraph ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) –1-1→ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
5	1 4	mp1i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USPGraph ↔ ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) –1-1→ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
6		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝐸 )
7	6	dmeqd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = dom 𝐸 )
8		opvtxfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9	8	pweqd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝒫 𝑉 )
10	9	difeq1d	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) )
11	10	rabeqdv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } = { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } )
12	6 7 11	f1eq123d	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) : dom ( iEdg ‘ ⟨ 𝑉 , 𝐸 ⟩ ) –1-1→ { 𝑝 ∈ ( 𝒫 ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )
13	5 12	bitrd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐸 ∈ 𝑋 ) → ( ⟨ 𝑉 , 𝐸 ⟩ ∈ USPGraph ↔ 𝐸 : dom 𝐸 –1-1→ { 𝑝 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑝 ) ≤ 2 } ) )