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 = <. V , ( _I |` E ) >.
Assertion ushrisomgr 
|- ( G e. USHGraph -> G IsomGr H )

Proof

Step Hyp Ref Expression
1 ushrisomgr.v 
 |-  V = ( Vtx ` G )
2 ushrisomgr.e 
 |-  E = ( Edg ` G )
3 ushrisomgr.s 
 |-  H = <. V , ( _I |` E ) >.
4 1 fvexi 
 |-  V e. _V
5 4 a1i 
 |-  ( G e. USHGraph -> V e. _V )
6 5 resiexd 
 |-  ( G e. USHGraph -> ( _I |` V ) e. _V )
7 f1oi 
 |-  ( _I |` V ) : V -1-1-onto-> V
8 7 a1i 
 |-  ( G e. USHGraph -> ( _I |` V ) : V -1-1-onto-> V )
9 3 fveq2i 
 |-  ( Vtx ` H ) = ( Vtx ` <. V , ( _I |` E ) >. )
10 2 fvexi 
 |-  E e. _V
11 id 
 |-  ( E e. _V -> E e. _V )
12 11 resiexd 
 |-  ( E e. _V -> ( _I |` E ) e. _V )
13 10 12 ax-mp 
 |-  ( _I |` E ) e. _V
14 4 13 pm3.2i 
 |-  ( V e. _V /\ ( _I |` E ) e. _V )
15 opvtxfv 
 |-  ( ( V e. _V /\ ( _I |` E ) e. _V ) -> ( Vtx ` <. V , ( _I |` E ) >. ) = V )
16 14 15 mp1i 
 |-  ( G e. USHGraph -> ( Vtx ` <. V , ( _I |` E ) >. ) = V )
17 9 16 eqtrid 
 |-  ( G e. USHGraph -> ( Vtx ` H ) = V )
18 17 f1oeq3d 
 |-  ( G e. USHGraph -> ( ( _I |` V ) : V -1-1-onto-> ( Vtx ` H ) <-> ( _I |` V ) : V -1-1-onto-> V ) )
19 8 18 mpbird 
 |-  ( G e. USHGraph -> ( _I |` V ) : V -1-1-onto-> ( Vtx ` H ) )
20 fvexd 
 |-  ( G e. USHGraph -> ( iEdg ` G ) e. _V )
21 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
22 1 21 ushgrf 
 |-  ( G e. USHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P V \ { (/) } ) )
23 f1f1orn 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P V \ { (/) } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ran ( iEdg ` G ) )
24 22 23 syl 
 |-  ( G e. USHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ran ( iEdg ` G ) )
25 3 fveq2i 
 |-  ( iEdg ` H ) = ( iEdg ` <. V , ( _I |` E ) >. )
26 10 a1i 
 |-  ( G e. USHGraph -> E e. _V )
27 26 resiexd 
 |-  ( G e. USHGraph -> ( _I |` E ) e. _V )
28 opiedgfv 
 |-  ( ( V e. _V /\ ( _I |` E ) e. _V ) -> ( iEdg ` <. V , ( _I |` E ) >. ) = ( _I |` E ) )
29 4 27 28 sylancr 
 |-  ( G e. USHGraph -> ( iEdg ` <. V , ( _I |` E ) >. ) = ( _I |` E ) )
30 25 29 eqtrid 
 |-  ( G e. USHGraph -> ( iEdg ` H ) = ( _I |` E ) )
31 30 dmeqd 
 |-  ( G e. USHGraph -> dom ( iEdg ` H ) = dom ( _I |` E ) )
32 dmresi 
 |-  dom ( _I |` E ) = E
33 2 a1i 
 |-  ( G e. USHGraph -> E = ( Edg ` G ) )
34 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
35 33 34 eqtrdi 
 |-  ( G e. USHGraph -> E = ran ( iEdg ` G ) )
36 32 35 eqtrid 
 |-  ( G e. USHGraph -> dom ( _I |` E ) = ran ( iEdg ` G ) )
37 31 36 eqtrd 
 |-  ( G e. USHGraph -> dom ( iEdg ` H ) = ran ( iEdg ` G ) )
38 37 f1oeq3d 
 |-  ( G e. USHGraph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> ran ( iEdg ` G ) ) )
39 24 38 mpbird 
 |-  ( G e. USHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) )
40 ushgruhgr 
 |-  ( G e. USHGraph -> G e. UHGraph )
41 1 21 uhgrss 
 |-  ( ( G e. UHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) C_ V )
42 40 41 sylan 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) C_ V )
43 resiima 
 |-  ( ( ( iEdg ` G ) ` i ) C_ V -> ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
44 42 43 syl 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
45 f1f 
 |-  ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-> ( ~P V \ { (/) } ) -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
46 22 45 syl 
 |-  ( G e. USHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P V \ { (/) } ) )
47 46 ffund 
 |-  ( G e. USHGraph -> Fun ( iEdg ` G ) )
48 fvelrn 
 |-  ( ( Fun ( iEdg ` G ) /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) e. ran ( iEdg ` G ) )
49 47 48 sylan 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) e. ran ( iEdg ` G ) )
50 2 34 eqtri 
 |-  E = ran ( iEdg ` G )
51 49 50 eleqtrrdi 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( iEdg ` G ) ` i ) e. E )
52 fvresi 
 |-  ( ( ( iEdg ` G ) ` i ) e. E -> ( ( _I |` E ) ` ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
53 51 52 syl 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( _I |` E ) ` ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` G ) ` i ) )
54 10 a1i 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> E e. _V )
55 54 resiexd 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( _I |` E ) e. _V )
56 4 55 28 sylancr 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( iEdg ` <. V , ( _I |` E ) >. ) = ( _I |` E ) )
57 25 56 eqtr2id 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( _I |` E ) = ( iEdg ` H ) )
58 57 fveq1d 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( _I |` E ) ` ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) )
59 44 53 58 3eqtr2d 
 |-  ( ( G e. USHGraph /\ i e. dom ( iEdg ` G ) ) -> ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) )
60 59 ralrimiva 
 |-  ( G e. USHGraph -> A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) )
61 39 60 jca 
 |-  ( G e. USHGraph -> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) ) )
62 f1oeq1 
 |-  ( g = ( iEdg ` G ) -> ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> dom ( 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 |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) <-> ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) ) )
66 65 ralbidv 
 |-  ( g = ( iEdg ` G ) -> ( A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) <-> A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) ) )
67 62 66 anbi12d 
 |-  ( g = ( iEdg ` G ) -> ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) <-> ( ( iEdg ` G ) : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( ( iEdg ` G ) ` i ) ) ) ) )
68 20 61 67 spcedv 
 |-  ( G e. USHGraph -> E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) )
69 19 68 jca 
 |-  ( G e. USHGraph -> ( ( _I |` V ) : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) )
70 f1oeq1 
 |-  ( f = ( _I |` V ) -> ( f : V -1-1-onto-> ( Vtx ` H ) <-> ( _I |` V ) : V -1-1-onto-> ( Vtx ` H ) ) )
71 imaeq1 
 |-  ( f = ( _I |` V ) -> ( f " ( ( iEdg ` G ) ` i ) ) = ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) )
72 71 eqeq1d 
 |-  ( f = ( _I |` V ) -> ( ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) <-> ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) )
73 72 ralbidv 
 |-  ( f = ( _I |` V ) -> ( A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) <-> A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) )
74 73 anbi2d 
 |-  ( f = ( _I |` V ) -> ( ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) <-> ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) )
75 74 exbidv 
 |-  ( f = ( _I |` V ) -> ( E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) <-> E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) )
76 70 75 anbi12d 
 |-  ( f = ( _I |` V ) -> ( ( f : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) <-> ( ( _I |` V ) : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( _I |` V ) " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) ) )
77 6 69 76 spcedv 
 |-  ( G e. USHGraph -> E. f ( f : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) )
78 opex 
 |-  <. V , ( _I |` E ) >. e. _V
79 3 78 eqeltri 
 |-  H e. _V
80 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
81 eqid 
 |-  ( iEdg ` H ) = ( iEdg ` H )
82 1 80 21 81 isomgr 
 |-  ( ( G e. USHGraph /\ H e. _V ) -> ( G IsomGr H <-> E. f ( f : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) ) )
83 79 82 mpan2 
 |-  ( G e. USHGraph -> ( G IsomGr H <-> E. f ( f : V -1-1-onto-> ( Vtx ` H ) /\ E. g ( g : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( f " ( ( iEdg ` G ) ` i ) ) = ( ( iEdg ` H ) ` ( g ` i ) ) ) ) ) )
84 77 83 mpbird 
 |-  ( G e. USHGraph -> G IsomGr H )