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