This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
ausgrusgri.1 ⊢ 𝑂 = { 𝑓 ∣ 𝑓 : dom 𝑓 –1-1→ ran 𝑓 }
Assertion usgrausgrb ( ( 𝐻 ∈ 𝑊 ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ 𝐻 ∈ USGraph ) )

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
2 ausgrusgri.1 ⊢ 𝑂 = { 𝑓 ∣ 𝑓 : dom 𝑓 –1-1→ ran 𝑓 }
3 1 2 ausgrusgri ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → 𝐻 ∈ USGraph )
4 3 3exp ⊢ ( 𝐻 ∈ 𝑊 → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) → ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 → 𝐻 ∈ USGraph ) ) )
5 4 com23 ⊢ ( 𝐻 ∈ 𝑊 → ( ( iEdg ‘ 𝐻 ) ∈ 𝑂 → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) → 𝐻 ∈ USGraph ) ) )
6 5 imp ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) → 𝐻 ∈ USGraph ) )
7 1 usgrausgri ⊢ ( 𝐻 ∈ USGraph → ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) )
8 6 7 impbid1 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( iEdg ‘ 𝐻 ) ∈ 𝑂 ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ 𝐻 ∈ USGraph ) )