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 \subseteq \{x \in 𝒫 v \| \|x\| = 2\}\}$
		ausgrusgri.1	$⊢ O = \{f \| f : dom f \underset{1-1}{⟶} ran f\}$
	Assertion	usgrausgrb	$⊢ (H \in W \land iEdg (H) \in O) \to (Vtx (H) G Edg (H) \leftrightarrow H \in USGraph)$

Proof

Step	Hyp	Ref	Expression
1		ausgr.1	$⊢ G = \{⟨v, e⟩ \| e \subseteq \{x \in 𝒫 v \| \|x\| = 2\}\}$
2		ausgrusgri.1	$⊢ O = \{f \| f : dom f \underset{1-1}{⟶} ran f\}$
3	1 2	ausgrusgri	$⊢ (H \in W \land Vtx (H) G Edg (H) \land iEdg (H) \in O) \to H \in USGraph$
4	3	3exp	$⊢ H \in W \to (Vtx (H) G Edg (H) \to (iEdg (H) \in O \to H \in USGraph))$
5	4	com23	$⊢ H \in W \to (iEdg (H) \in O \to (Vtx (H) G Edg (H) \to H \in USGraph))$
6	5	imp	$⊢ (H \in W \land iEdg (H) \in O) \to (Vtx (H) G Edg (H) \to H \in USGraph)$
7	1	usgrausgri	$⊢ H \in USGraph \to Vtx (H) G Edg (H)$
8	6 7	impbid1	$⊢ (H \in W \land iEdg (H) \in O) \to (Vtx (H) G Edg (H) \leftrightarrow H \in USGraph)$