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 ⊢G=ve|e⊆x∈𝒫v|x=2
Assertion ausgrumgri ⊢H∈W∧Vtx⁡HGEdg⁡H∧Fun⁡iEdg⁡H→H∈UMGraph

Proof

Step Hyp Ref Expression
1 ausgr.1 ⊢G=ve|e⊆x∈𝒫v|x=2
2 fvex ⊢Vtx⁡H∈V
3 fvex ⊢Edg⁡H∈V
4 1 isausgr ⊢Vtx⁡H∈V∧Edg⁡H∈V→Vtx⁡HGEdg⁡H↔Edg⁡H⊆x∈𝒫Vtx⁡H|x=2
5 2 3 4 mp2an ⊢Vtx⁡HGEdg⁡H↔Edg⁡H⊆x∈𝒫Vtx⁡H|x=2
6 edgval ⊢Edg⁡H=ran⁡iEdg⁡H
7 6 a1i ⊢H∈W→Edg⁡H=ran⁡iEdg⁡H
8 7 sseq1d ⊢H∈W→Edg⁡H⊆x∈𝒫Vtx⁡H|x=2↔ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2
9 funfn ⊢Fun⁡iEdg⁡H↔iEdg⁡HFndom⁡iEdg⁡H
10 9 biimpi ⊢Fun⁡iEdg⁡H→iEdg⁡HFndom⁡iEdg⁡H
11 10 3ad2ant3 ⊢H∈W∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2∧Fun⁡iEdg⁡H→iEdg⁡HFndom⁡iEdg⁡H
12 simp2 ⊢H∈W∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2∧Fun⁡iEdg⁡H→ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2
13 df-f ⊢iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2↔iEdg⁡HFndom⁡iEdg⁡H∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2
14 11 12 13 sylanbrc ⊢H∈W∧ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2∧Fun⁡iEdg⁡H→iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
15 14 3exp ⊢H∈W→ran⁡iEdg⁡H⊆x∈𝒫Vtx⁡H|x=2→Fun⁡iEdg⁡H→iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
16 8 15 sylbid ⊢H∈W→Edg⁡H⊆x∈𝒫Vtx⁡H|x=2→Fun⁡iEdg⁡H→iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
17 5 16 biimtrid ⊢H∈W→Vtx⁡HGEdg⁡H→Fun⁡iEdg⁡H→iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
18 17 3imp ⊢H∈W∧Vtx⁡HGEdg⁡H∧Fun⁡iEdg⁡H→iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
19 eqid ⊢Vtx⁡H=Vtx⁡H
20 eqid ⊢iEdg⁡H=iEdg⁡H
21 19 20 isumgrs ⊢H∈W→H∈UMGraph↔iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
22 21 3ad2ant1 ⊢H∈W∧Vtx⁡HGEdg⁡H∧Fun⁡iEdg⁡H→H∈UMGraph↔iEdg⁡H:dom⁡iEdg⁡H⟶x∈𝒫Vtx⁡H|x=2
23 18 22 mpbird ⊢H∈W∧Vtx⁡HGEdg⁡H∧Fun⁡iEdg⁡H→H∈UMGraph