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

Proof

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