Metamath Proof Explorer

Theorem ausgrumgri

Description: If an alternatively defined simple graph has the vertices and edges of an arbitrary graph, the arbitrary graph is an undirected multigraph. (Contributed by AV, 18-Oct-2020) (Revised by AV, 25-Nov-2020)

Ref Expression
Hypothesis ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
Assertion ausgrumgri ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ Fun ( iEdg ‘ 𝐻 ) ) → 𝐻 ∈ UMGraph )

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢ 𝐺 = { ⟨ 𝑣 , 𝑒 ⟩ ∣ 𝑒 ⊆ { 𝑥 ∈ 𝒫 𝑣 ∣ ( ♯ ‘ 𝑥 ) = 2 } }
2 fvex ⊢ ( Vtx ‘ 𝐻 ) ∈ V
3 fvex ⊢ ( Edg ‘ 𝐻 ) ∈ V
4 1 isausgr ⊢ ( ( ( Vtx ‘ 𝐻 ) ∈ V ∧ ( Edg ‘ 𝐻 ) ∈ V ) → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
5 2 3 4 mp2an ⊢ ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ↔ ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 edgval ⊢ ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 )
7 6 a1i ⊢ ( 𝐻 ∈ 𝑊 → ( Edg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐻 ) )
8 7 sseq1d ⊢ ( 𝐻 ∈ 𝑊 → ( ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
9 funfn ⊢ ( Fun ( iEdg ‘ 𝐻 ) ↔ ( iEdg ‘ 𝐻 ) Fn dom ( iEdg ‘ 𝐻 ) )
10 9 biimpi ⊢ ( Fun ( iEdg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) Fn dom ( iEdg ‘ 𝐻 ) )
11 10 3ad2ant3 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ Fun ( iEdg ‘ 𝐻 ) ) → ( iEdg ‘ 𝐻 ) Fn dom ( iEdg ‘ 𝐻 ) )
12 simp2 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ Fun ( iEdg ‘ 𝐻 ) ) → ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
13 df-f ⊢ ( ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( ( iEdg ‘ 𝐻 ) Fn dom ( iEdg ‘ 𝐻 ) ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
14 11 12 13 sylanbrc ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ Fun ( iEdg ‘ 𝐻 ) ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
15 14 3exp ⊢ ( 𝐻 ∈ 𝑊 → ( ran ( iEdg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( Fun ( iEdg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
16 8 15 sylbid ⊢ ( 𝐻 ∈ 𝑊 → ( ( Edg ‘ 𝐻 ) ⊆ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( Fun ( iEdg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
17 5 16 syl5bi ⊢ ( 𝐻 ∈ 𝑊 → ( ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) → ( Fun ( iEdg ‘ 𝐻 ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) ) )
18 17 3imp ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ Fun ( iEdg ‘ 𝐻 ) ) → ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
19 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
20 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
21 19 20 isumgrs ⊢ ( 𝐻 ∈ 𝑊 → ( 𝐻 ∈ UMGraph ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
22 21 3ad2ant1 ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ Fun ( iEdg ‘ 𝐻 ) ) → ( 𝐻 ∈ UMGraph ↔ ( iEdg ‘ 𝐻 ) : dom ( iEdg ‘ 𝐻 ) ⟶ { 𝑥 ∈ 𝒫 ( Vtx ‘ 𝐻 ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
23 18 22 mpbird ⊢ ( ( 𝐻 ∈ 𝑊 ∧ ( Vtx ‘ 𝐻 ) 𝐺 ( Edg ‘ 𝐻 ) ∧ Fun ( iEdg ‘ 𝐻 ) ) → 𝐻 ∈ UMGraph )