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

Metamath Proof Explorer

Theorem usgrausgri

Description: A simple graph represented by an alternatively defined simple graph. (Contributed by AV, 15-Oct-2020)

Ref Expression
Hypothesis ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
Assertion usgrausgri ( 𝐻 ∈ USGraph → ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
2 usgredgss ⊢ ( 𝐻 ∈ USGraph → ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
3 fvex ⊢ ( Vtx ‘ 𝐻 ) ∈ V
4 fvex ⊢ ( Edg ‘ 𝐻 ) ∈ V
5 1 isausgr ⊢ ( ( ( Vtx ‘ 𝐻 ) ∈ V ∧ ( Edg ‘ 𝐻 ) ∈ V ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
6 3 4 5 mp2an ⊢ ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
7 2 6 sylibr ⊢ ( 𝐻 ∈ USGraph → ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) )