Metamath Proof Explorer

Theorem ushggricedg

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 ushggricedg.v 
|- V = ( Vtx ` G )
ushggricedg.e 
|- E = ( Edg ` G )
ushggricedg.s 
|- H = <. V , ( _I |` E ) >.
Assertion ushggricedg 
|- ( G e. USHGraph -> G ~=gr H )

Proof

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