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