Metamath Proof Explorer

Theorem ushrisomgr

Description: A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022)

Ref Expression
Hypotheses ushrisomgr.v ⊢V=Vtx⁡G
ushrisomgr.e ⊢E=Edg⁡G
ushrisomgr.s ⊢H=VI↾E
Assertion ushrisomgr ⊢G∈USHGraph→GIsomGrH

Proof

Step Hyp Ref Expression
1 ushrisomgr.v ⊢V=Vtx⁡G
2 ushrisomgr.e ⊢E=Edg⁡G
3 ushrisomgr.s ⊢H=VI↾E
4 1 fvexi ⊢V∈V
5 4 a1i ⊢G∈USHGraph→V∈V
6 5 resiexd ⊢G∈USHGraph→I↾V∈V
7 f1oi ⊢I↾V:V⟶1-1 ontoV
8 7 a1i ⊢G∈USHGraph→I↾V:V⟶1-1 ontoV
9 3 fveq2i ⊢Vtx⁡H=Vtx⁡VI↾E
10 2 fvexi ⊢E∈V
11 id ⊢E∈V→E∈V
12 11 resiexd ⊢E∈V→I↾E∈V
13 10 12 ax-mp ⊢I↾E∈V
14 4 13 pm3.2i ⊢V∈V∧I↾E∈V
15 opvtxfv ⊢V∈V∧I↾E∈V→Vtx⁡VI↾E=V
16 14 15 mp1i ⊢G∈USHGraph→Vtx⁡VI↾E=V
17 9 16 eqtrid ⊢G∈USHGraph→Vtx⁡H=V
18 17 f1oeq3d ⊢G∈USHGraph→I↾V:V⟶1-1 ontoVtx⁡H↔I↾V:V⟶1-1 ontoV
19 8 18 mpbird ⊢G∈USHGraph→I↾V:V⟶1-1 ontoVtx⁡H
20 fvexd ⊢G∈USHGraph→iEdg⁡G∈V
21 eqid ⊢iEdg⁡G=iEdg⁡G
22 1 21 ushgrf ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1𝒫V∖∅
23 f1f1orn ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1𝒫V∖∅→iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontoran⁡iEdg⁡G
24 22 23 syl ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontoran⁡iEdg⁡G
25 3 fveq2i ⊢iEdg⁡H=iEdg⁡VI↾E
26 10 a1i ⊢G∈USHGraph→E∈V
27 26 resiexd ⊢G∈USHGraph→I↾E∈V
28 opiedgfv ⊢V∈V∧I↾E∈V→iEdg⁡VI↾E=I↾E
29 4 27 28 sylancr ⊢G∈USHGraph→iEdg⁡VI↾E=I↾E
30 25 29 eqtrid ⊢G∈USHGraph→iEdg⁡H=I↾E
31 30 dmeqd ⊢G∈USHGraph→dom⁡iEdg⁡H=dom⁡I↾E
32 dmresi ⊢dom⁡I↾E=E
33 2 a1i ⊢G∈USHGraph→E=Edg⁡G
34 edgval ⊢Edg⁡G=ran⁡iEdg⁡G
35 33 34 eqtrdi ⊢G∈USHGraph→E=ran⁡iEdg⁡G
36 32 35 eqtrid ⊢G∈USHGraph→dom⁡I↾E=ran⁡iEdg⁡G
37 31 36 eqtrd ⊢G∈USHGraph→dom⁡iEdg⁡H=ran⁡iEdg⁡G
38 37 f1oeq3d ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontoran⁡iEdg⁡G
39 24 38 mpbird ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H
40 ushgruhgr ⊢G∈USHGraph→G∈UHGraph
41 1 21 uhgrss ⊢G∈UHGraph∧i∈dom⁡iEdg⁡G→iEdg⁡G⁡i⊆V
42 40 41 sylan ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→iEdg⁡G⁡i⊆V
43 resiima ⊢iEdg⁡G⁡i⊆V→I↾ViEdg⁡G⁡i=iEdg⁡G⁡i
44 42 43 syl ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→I↾ViEdg⁡G⁡i=iEdg⁡G⁡i
45 f1f ⊢iEdg⁡G:dom⁡iEdg⁡G⟶1-1𝒫V∖∅→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫V∖∅
46 22 45 syl ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶𝒫V∖∅
47 46 ffund ⊢G∈USHGraph→Fun⁡iEdg⁡G
48 fvelrn ⊢Fun⁡iEdg⁡G∧i∈dom⁡iEdg⁡G→iEdg⁡G⁡i∈ran⁡iEdg⁡G
49 47 48 sylan ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→iEdg⁡G⁡i∈ran⁡iEdg⁡G
50 2 34 eqtri ⊢E=ran⁡iEdg⁡G
51 49 50 eleqtrrdi ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→iEdg⁡G⁡i∈E
52 fvresi ⊢iEdg⁡G⁡i∈E→I↾E⁡iEdg⁡G⁡i=iEdg⁡G⁡i
53 51 52 syl ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→I↾E⁡iEdg⁡G⁡i=iEdg⁡G⁡i
54 10 a1i ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→E∈V
55 54 resiexd ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→I↾E∈V
56 4 55 28 sylancr ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→iEdg⁡VI↾E=I↾E
57 25 56 eqtr2id ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→I↾E=iEdg⁡H
58 57 fveq1d ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→I↾E⁡iEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
59 44 53 58 3eqtr2d ⊢G∈USHGraph∧i∈dom⁡iEdg⁡G→I↾ViEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
60 59 ralrimiva ⊢G∈USHGraph→∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
61 39 60 jca ⊢G∈USHGraph→iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
62 f1oeq1 ⊢g=iEdg⁡G→g:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H
63 fveq1 ⊢g=iEdg⁡G→g⁡i=iEdg⁡G⁡i
64 63 fveq2d ⊢g=iEdg⁡G→iEdg⁡H⁡g⁡i=iEdg⁡H⁡iEdg⁡G⁡i
65 64 eqeq2d ⊢g=iEdg⁡G→I↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔I↾ViEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
66 65 ralbidv ⊢g=iEdg⁡G→∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
67 62 66 anbi12d ⊢g=iEdg⁡G→g:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔iEdg⁡G:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡iEdg⁡G⁡i
68 20 61 67 spcedv ⊢G∈USHGraph→∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
69 19 68 jca ⊢G∈USHGraph→I↾V:V⟶1-1 ontoVtx⁡H∧∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
70 f1oeq1 ⊢f=I↾V→f:V⟶1-1 ontoVtx⁡H↔I↾V:V⟶1-1 ontoVtx⁡H
71 imaeq1 ⊢f=I↾V→fiEdg⁡G⁡i=I↾ViEdg⁡G⁡i
72 71 eqeq1d ⊢f=I↾V→fiEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔I↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
73 72 ralbidv ⊢f=I↾V→∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
74 73 anbi2d ⊢f=I↾V→g:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔g:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
75 74 exbidv ⊢f=I↾V→∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
76 70 75 anbi12d ⊢f=I↾V→f:V⟶1-1 ontoVtx⁡H∧∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i↔I↾V:V⟶1-1 ontoVtx⁡H∧∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GI↾ViEdg⁡G⁡i=iEdg⁡H⁡g⁡i
77 6 69 76 spcedv ⊢G∈USHGraph→∃ff:V⟶1-1 ontoVtx⁡H∧∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i
78 opex ⊢VI↾E∈V
79 3 78 eqeltri ⊢H∈V
80 eqid ⊢Vtx⁡H=Vtx⁡H
81 eqid ⊢iEdg⁡H=iEdg⁡H
82 1 80 21 81 isomgr ⊢G∈USHGraph∧H∈V→GIsomGrH↔∃ff:V⟶1-1 ontoVtx⁡H∧∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i
83 79 82 mpan2 ⊢G∈USHGraph→GIsomGrH↔∃ff:V⟶1-1 ontoVtx⁡H∧∃gg:dom⁡iEdg⁡G⟶1-1 ontodom⁡iEdg⁡H∧∀i∈dom⁡iEdg⁡GfiEdg⁡G⁡i=iEdg⁡H⁡g⁡i
84 77 83 mpbird ⊢G∈USHGraph→GIsomGrH