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

Metamath Proof Explorer

Theorem usgrop

Description: A simple graph represented by an ordered pair. (Contributed by AV, 23-Oct-2020) (Proof shortened by AV, 30-Nov-2020)

Ref Expression
Assertion usgrop ( 𝐺 ∈ USGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 usgrfs ⊢ ( 𝐺 ∈ USGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
4 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
5 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
6 4 5 pm3.2i ⊢ ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V )
7 isusgrop ⊢ ( ( ( Vtx ‘ 𝐺 ) ∈ V ∧ ( iEdg ‘ 𝐺 ) ∈ V ) → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
8 6 7 mp1i ⊢ ( 𝐺 ∈ USGraph → ( ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
9 3 8 mpbird ⊢ ( 𝐺 ∈ USGraph → ⟨ ( Vtx ‘ 𝐺 ) , ( iEdg ‘ 𝐺 ) ⟩ ∈ USGraph )