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

Metamath Proof Explorer

Theorem gropeld

Description: If any representation of a graph with vertices V and edges E is an element of an arbitrary class C , then the ordered pair <. V , E >. of the set of vertices and the set of edges (which is such a representation of a graph with vertices V and edges E ) is an element of this class C . (Contributed by AV, 11-Oct-2020)

	Ref	Expression
Hypotheses	gropeld.g	⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝑔 ∈ 𝐶 ) )
	gropeld.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
	gropeld.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
Assertion	gropeld	⊢ ( 𝜑 → ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		gropeld.g	⊢ ( 𝜑 → ∀ 𝑔 ( ( ( Vtx ‘ 𝑔 ) = 𝑉 ∧ ( iEdg ‘ 𝑔 ) = 𝐸 ) → 𝑔 ∈ 𝐶 ) )
2		gropeld.v	⊢ ( 𝜑 → 𝑉 ∈ 𝑈 )
3		gropeld.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑊 )
4	1 2 3	gropd	⊢ ( 𝜑 → [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝑔 ∈ 𝐶 )
5		sbcel1v	⊢ ( [ ⟨ 𝑉 , 𝐸 ⟩ / 𝑔 ] 𝑔 ∈ 𝐶 ↔ ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐶 )
6	4 5	sylib	⊢ ( 𝜑 → ⟨ 𝑉 , 𝐸 ⟩ ∈ 𝐶 )