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 ) )