Metamath Proof Explorer

Theorem isomgreqve

Description: A set is isomorphic to a hypergraph if it has the same vertices and the same edges. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgreqve 
|- ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> A IsomGr B )

Proof

Step Hyp Ref Expression
1 fvexd 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( Vtx ` B ) e. _V )
2 1 resiexd 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( _I |` ( Vtx ` B ) ) e. _V )
3 f1oi 
 |-  ( _I |` ( Vtx ` B ) ) : ( Vtx ` B ) -1-1-onto-> ( Vtx ` B )
4 simprl 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( Vtx ` A ) = ( Vtx ` B ) )
5 4 f1oeq2d 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( ( _I |` ( Vtx ` B ) ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) <-> ( _I |` ( Vtx ` B ) ) : ( Vtx ` B ) -1-1-onto-> ( Vtx ` B ) ) )
6 3 5 mpbiri 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( _I |` ( Vtx ` B ) ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) )
7 fvexd 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( iEdg ` B ) e. _V )
8 7 dmexd 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> dom ( iEdg ` B ) e. _V )
9 8 resiexd 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( _I |` dom ( iEdg ` B ) ) e. _V )
10 f1oi 
 |-  ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` B )
11 simprr 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( iEdg ` A ) = ( iEdg ` B ) )
12 11 dmeqd 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> dom ( iEdg ` A ) = dom ( iEdg ` B ) )
13 12 f1oeq2d 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) <-> ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` B ) ) )
14 10 13 mpbiri 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) )
15 eqid 
 |-  ( Vtx ` A ) = ( Vtx ` A )
16 eqid 
 |-  ( iEdg ` A ) = ( iEdg ` A )
17 15 16 uhgrss 
 |-  ( ( A e. UHGraph /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` A ) )
18 17 ad4ant14 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` A ) )
19 sseq2 
 |-  ( ( Vtx ` A ) = ( Vtx ` B ) -> ( ( ( iEdg ` A ) ` i ) C_ ( Vtx ` A ) <-> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` B ) ) )
20 19 adantr 
 |-  ( ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) -> ( ( ( iEdg ` A ) ` i ) C_ ( Vtx ` A ) <-> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` B ) ) )
21 20 adantl 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( ( ( iEdg ` A ) ` i ) C_ ( Vtx ` A ) <-> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` B ) ) )
22 21 adantr 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( ( iEdg ` A ) ` i ) C_ ( Vtx ` A ) <-> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` B ) ) )
23 18 22 mpbid 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` i ) C_ ( Vtx ` B ) )
24 resiima 
 |-  ( ( ( iEdg ` A ) ` i ) C_ ( Vtx ` B ) -> ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` A ) ` i ) )
25 23 24 syl 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` A ) ` i ) )
26 fvresi 
 |-  ( i e. dom ( iEdg ` A ) -> ( ( _I |` dom ( iEdg ` A ) ) ` i ) = i )
27 26 adantl 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( _I |` dom ( iEdg ` A ) ) ` i ) = i )
28 27 fveq2d 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` ( ( _I |` dom ( iEdg ` A ) ) ` i ) ) = ( ( iEdg ` A ) ` i ) )
29 id 
 |-  ( ( iEdg ` A ) = ( iEdg ` B ) -> ( iEdg ` A ) = ( iEdg ` B ) )
30 dmeq 
 |-  ( ( iEdg ` A ) = ( iEdg ` B ) -> dom ( iEdg ` A ) = dom ( iEdg ` B ) )
31 30 reseq2d 
 |-  ( ( iEdg ` A ) = ( iEdg ` B ) -> ( _I |` dom ( iEdg ` A ) ) = ( _I |` dom ( iEdg ` B ) ) )
32 31 fveq1d 
 |-  ( ( iEdg ` A ) = ( iEdg ` B ) -> ( ( _I |` dom ( iEdg ` A ) ) ` i ) = ( ( _I |` dom ( iEdg ` B ) ) ` i ) )
33 29 32 fveq12d 
 |-  ( ( iEdg ` A ) = ( iEdg ` B ) -> ( ( iEdg ` A ) ` ( ( _I |` dom ( iEdg ` A ) ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
34 33 adantl 
 |-  ( ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) -> ( ( iEdg ` A ) ` ( ( _I |` dom ( iEdg ` A ) ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
35 34 adantl 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( ( iEdg ` A ) ` ( ( _I |` dom ( iEdg ` A ) ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
36 35 adantr 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` ( ( _I |` dom ( iEdg ` A ) ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
37 25 28 36 3eqtr2d 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) /\ i e. dom ( iEdg ` A ) ) -> ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
38 37 ralrimiva 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
39 14 38 jca 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) ) )
40 f1oeq1 
 |-  ( g = ( _I |` dom ( iEdg ` B ) ) -> ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) <-> ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) ) )
41 fveq1 
 |-  ( g = ( _I |` dom ( iEdg ` B ) ) -> ( g ` i ) = ( ( _I |` dom ( iEdg ` B ) ) ` i ) )
42 41 fveq2d 
 |-  ( g = ( _I |` dom ( iEdg ` B ) ) -> ( ( iEdg ` B ) ` ( g ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) )
43 42 eqeq2d 
 |-  ( g = ( _I |` dom ( iEdg ` B ) ) -> ( ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) ) )
44 43 ralbidv 
 |-  ( g = ( _I |` dom ( iEdg ` B ) ) -> ( A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) ) )
45 40 44 anbi12d 
 |-  ( g = ( _I |` dom ( iEdg ` B ) ) -> ( ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) <-> ( ( _I |` dom ( iEdg ` B ) ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( ( _I |` dom ( iEdg ` B ) ) ` i ) ) ) ) )
46 9 39 45 spcedv 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) )
47 6 46 jca 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( ( _I |` ( Vtx ` B ) ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) )
48 f1oeq1 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) <-> ( _I |` ( Vtx ` B ) ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) )
49 imaeq1 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( f " ( ( iEdg ` A ) ` i ) ) = ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) )
50 49 eqeq1d 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) )
51 50 ralbidv 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) )
52 51 anbi2d 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) <-> ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) )
53 52 exbidv 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) <-> E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) )
54 48 53 anbi12d 
 |-  ( f = ( _I |` ( Vtx ` B ) ) -> ( ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) <-> ( ( _I |` ( Vtx ` B ) ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( ( _I |` ( Vtx ` B ) ) " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) ) )
55 2 47 54 spcedv 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> E. f ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) )
56 eqid 
 |-  ( Vtx ` B ) = ( Vtx ` B )
57 eqid 
 |-  ( iEdg ` B ) = ( iEdg ` B )
58 15 56 16 57 isomgr 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( A IsomGr B <-> E. f ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) ) )
59 58 adantr 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> ( A IsomGr B <-> E. f ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ E. g ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) ) )
60 55 59 mpbird 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( ( Vtx ` A ) = ( Vtx ` B ) /\ ( iEdg ` A ) = ( iEdg ` B ) ) ) -> A IsomGr B )