Metamath Proof Explorer

Theorem isomgrtr

Description: The isomorphy relation is transitive for hypergraphs. (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtr 
|- ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( ( A IsomGr B /\ B IsomGr C ) -> A IsomGr C ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` A ) = ( Vtx ` A )
2 eqid 
 |-  ( Vtx ` B ) = ( Vtx ` B )
3 eqid 
 |-  ( iEdg ` A ) = ( iEdg ` A )
4 eqid 
 |-  ( iEdg ` B ) = ( iEdg ` B )
5 1 2 3 4 isomgr 
 |-  ( ( A e. UHGraph /\ B e. UHGraph ) -> ( 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 ) ) ) ) ) )
6 5 3adant3 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( 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 ) ) ) ) ) )
7 eqid 
 |-  ( Vtx ` C ) = ( Vtx ` C )
8 eqid 
 |-  ( iEdg ` C ) = ( iEdg ` C )
9 2 7 4 8 isomgr 
 |-  ( ( B e. UHGraph /\ C e. X ) -> ( B IsomGr C <-> E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) )
10 9 3adant1 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( B IsomGr C <-> E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) )
11 6 10 anbi12d 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( ( A IsomGr B /\ B IsomGr C ) <-> ( 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 ) ) ) ) /\ E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) ) )
12 vex 
 |-  v e. _V
13 vex 
 |-  f e. _V
14 12 13 coex 
 |-  ( v o. f ) e. _V
15 14 a1i 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> ( v o. f ) e. _V )
16 simpl 
 |-  ( ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) )
17 simprl 
 |-  ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) -> f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) )
18 f1oco 
 |-  ( ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) -> ( v o. f ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) )
19 16 17 18 syl2anr 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> ( v o. f ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) )
20 vex 
 |-  w e. _V
21 vex 
 |-  g e. _V
22 20 21 coex 
 |-  ( w o. g ) e. _V
23 22 a1i 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> ( w o. g ) e. _V )
24 simpl 
 |-  ( ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) )
25 simprl 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( 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 ) )
26 f1oco 
 |-  ( ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) ) -> ( w o. g ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) )
27 24 25 26 syl2anr 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> ( w o. g ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) )
28 isomgrtrlem 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) )
29 27 28 jca 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> ( ( w o. g ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) ) )
30 f1oeq1 
 |-  ( h = ( w o. g ) -> ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) <-> ( w o. g ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) ) )
31 fveq1 
 |-  ( h = ( w o. g ) -> ( h ` j ) = ( ( w o. g ) ` j ) )
32 31 fveq2d 
 |-  ( h = ( w o. g ) -> ( ( iEdg ` C ) ` ( h ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) )
33 32 eqeq2d 
 |-  ( h = ( w o. g ) -> ( ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) <-> ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) ) )
34 33 ralbidv 
 |-  ( h = ( w o. g ) -> ( A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) <-> A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) ) )
35 30 34 anbi12d 
 |-  ( h = ( w o. g ) -> ( ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) <-> ( ( w o. g ) : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) ) ) )
36 23 29 35 spcedv 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) )
37 36 ex 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) -> ( ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) )
38 37 exlimdv 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( 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. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) )
39 38 ex 
 |-  ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) -> ( ( 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. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
40 39 exlimdv 
 |-  ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) -> ( 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. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
41 40 3exp 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) -> ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) -> ( 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. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) ) ) )
42 41 com34 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( 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 ) ) ) -> ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) -> ( E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) ) ) )
43 42 imp32 
 |-  ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) -> ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) -> ( E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
44 43 imp32 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) )
45 19 44 jca 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> ( ( v o. f ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) )
46 f1oeq1 
 |-  ( e = ( v o. f ) -> ( e : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) <-> ( v o. f ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) ) )
47 imaeq1 
 |-  ( e = ( v o. f ) -> ( e " ( ( iEdg ` A ) ` j ) ) = ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) )
48 47 eqeq1d 
 |-  ( e = ( v o. f ) -> ( ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) <-> ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) )
49 48 ralbidv 
 |-  ( e = ( v o. f ) -> ( A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) <-> A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) )
50 49 anbi2d 
 |-  ( e = ( v o. f ) -> ( ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) <-> ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) )
51 50 exbidv 
 |-  ( e = ( v o. f ) -> ( E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) <-> E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) )
52 46 51 anbi12d 
 |-  ( e = ( v o. f ) -> ( ( e : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) <-> ( ( v o. f ) : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
53 15 45 52 spcedv 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> E. e ( e : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) )
54 1 7 3 8 isomgr 
 |-  ( ( A e. UHGraph /\ C e. X ) -> ( A IsomGr C <-> E. e ( e : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
55 54 3adant2 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( A IsomGr C <-> E. e ( e : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
56 55 ad2antrr 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> ( A IsomGr C <-> E. e ( e : ( Vtx ` A ) -1-1-onto-> ( Vtx ` C ) /\ E. h ( h : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` C ) /\ A. j e. dom ( iEdg ` A ) ( e " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( h ` j ) ) ) ) ) )
57 53 56 mpbird 
 |-  ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) /\ ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> A IsomGr C )
58 57 ex 
 |-  ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) -> ( ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A IsomGr C ) )
59 58 exlimdv 
 |-  ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ ( 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 ) ) ) ) ) -> ( E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A IsomGr C ) )
60 59 ex 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( ( 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 ) ) ) ) -> ( E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A IsomGr C ) ) )
61 60 exlimdv 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( 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 ) ) ) ) -> ( E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A IsomGr C ) ) )
62 61 impd 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( ( 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 ) ) ) ) /\ E. v ( v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) /\ E. w ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) ) -> A IsomGr C ) )
63 11 62 sylbid 
 |-  ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) -> ( ( A IsomGr B /\ B IsomGr C ) -> A IsomGr C ) )