Metamath Proof Explorer

Theorem usgrausgrb

Description: The equivalence of the definitions of a simple graph, expressed with the set of vertices and the set of edges. (Contributed by AV, 2-Jan-2020) (Revised by AV, 15-Oct-2020)

Ref Expression
Hypotheses ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
ausgrusgri.1 ⊢ O = f | f : dom ⁡ f ⟶ 1-1 ran ⁡ f
Assertion usgrausgrb ⊢ H ∈ W ∧ iEdg ⁡ H ∈ O → Vtx ⁡ H G Edg ⁡ H ↔ H ∈ USGraph

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
2 ausgrusgri.1 ⊢ O = f | f : dom ⁡ f ⟶ 1-1 ran ⁡ f
3 1 2 ausgrusgri ⊢ H ∈ W ∧ Vtx ⁡ H G Edg ⁡ H ∧ iEdg ⁡ H ∈ O → H ∈ USGraph
4 3 3exp ⊢ H ∈ W → Vtx ⁡ H G Edg ⁡ H → iEdg ⁡ H ∈ O → H ∈ USGraph
5 4 com23 ⊢ H ∈ W → iEdg ⁡ H ∈ O → Vtx ⁡ H G Edg ⁡ H → H ∈ USGraph
6 5 imp ⊢ H ∈ W ∧ iEdg ⁡ H ∈ O → Vtx ⁡ H G Edg ⁡ H → H ∈ USGraph
7 1 usgrausgri ⊢ H ∈ USGraph → Vtx ⁡ H G Edg ⁡ H
8 6 7 impbid1 ⊢ H ∈ W ∧ iEdg ⁡ H ∈ O → Vtx ⁡ H G Edg ⁡ H ↔ H ∈ USGraph