Metamath Proof Explorer

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 ⊢V∈W∧E∈X→VE∈USHGraph↔E:dom⁡E⟶1-1p∈𝒫V∖∅|p≤2

Proof

Step Hyp Ref Expression
1 opex ⊢VE∈V
2 eqid ⊢Vtx⁡VE=Vtx⁡VE
3 eqid ⊢iEdg⁡VE=iEdg⁡VE
4 2 3 isuspgr ⊢VE∈V→VE∈USHGraph↔iEdg⁡VE:dom⁡iEdg⁡VE⟶1-1p∈𝒫Vtx⁡VE∖∅|p≤2
5 1 4 mp1i ⊢V∈W∧E∈X→VE∈USHGraph↔iEdg⁡VE:dom⁡iEdg⁡VE⟶1-1p∈𝒫Vtx⁡VE∖∅|p≤2
6 opiedgfv ⊢V∈W∧E∈X→iEdg⁡VE=E
7 6 dmeqd ⊢V∈W∧E∈X→dom⁡iEdg⁡VE=dom⁡E
8 opvtxfv ⊢V∈W∧E∈X→Vtx⁡VE=V
9 8 pweqd ⊢V∈W∧E∈X→𝒫Vtx⁡VE=𝒫V
10 9 difeq1d ⊢V∈W∧E∈X→𝒫Vtx⁡VE∖∅=𝒫V∖∅
11 10 rabeqdv ⊢V∈W∧E∈X→p∈𝒫Vtx⁡VE∖∅|p≤2=p∈𝒫V∖∅|p≤2
12 6 7 11 f1eq123d ⊢V∈W∧E∈X→iEdg⁡VE:dom⁡iEdg⁡VE⟶1-1p∈𝒫Vtx⁡VE∖∅|p≤2↔E:dom⁡E⟶1-1p∈𝒫V∖∅|p≤2
13 5 12 bitrd ⊢V∈W∧E∈X→VE∈USHGraph↔E:dom⁡E⟶1-1p∈𝒫V∖∅|p≤2