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 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
Assertion usgrausgri ⊢ H ∈ USGraph → Vtx ⁡ H G Edg ⁡ H

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ G = v e | e ⊆ x ∈ 𝒫 v | x = 2
2 usgredgss ⊢ H ∈ USGraph → Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
3 fvex ⊢ Vtx ⁡ H ∈ V
4 fvex ⊢ Edg ⁡ H ∈ V
5 1 isausgr ⊢ Vtx ⁡ H ∈ V ∧ Edg ⁡ H ∈ V → Vtx ⁡ H G Edg ⁡ H ↔ Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
6 3 4 5 mp2an ⊢ Vtx ⁡ H G Edg ⁡ H ↔ Edg ⁡ H ⊆ x ∈ 𝒫 Vtx ⁡ H | x = 2
7 2 6 sylibr ⊢ H ∈ USGraph → Vtx ⁡ H G Edg ⁡ H