Metamath Proof Explorer

Theorem isomgrsym

Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgrsym 
|- ( ( A e. UHGraph /\ B e. Y ) -> ( A IsomGr B -> B IsomGr A ) )

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. 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 ) ) ) ) ) )
6 vex 
 |-  f e. _V
7 6 cnvex 
 |-  `' f e. _V
8 7 a1i 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 e. _V )
9 f1ocnv 
 |-  ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) -> `' f : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) )
10 9 adantr 
 |-  ( ( 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 ` B ) -1-1-onto-> ( Vtx ` A ) )
11 10 adantl 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ` B ) -1-1-onto-> ( Vtx ` A ) )
12 vex 
 |-  g e. _V
13 12 cnvex 
 |-  `' g e. _V
14 13 a1i 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) -> `' g e. _V )
15 f1ocnv 
 |-  ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) -> `' g : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) )
16 15 adantr 
 |-  ( ( 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 ` B ) -1-1-onto-> dom ( iEdg ` A ) )
17 16 3ad2ant2 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) -> `' g : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) )
18 f1ocnvdm 
 |-  ( ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ j e. dom ( iEdg ` B ) ) -> ( `' g ` j ) e. dom ( iEdg ` A ) )
19 18 3ad2antl2 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( `' g ` j ) e. dom ( iEdg ` A ) )
20 fveq2 
 |-  ( i = ( `' g ` j ) -> ( ( iEdg ` A ) ` i ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) )
21 20 imaeq2d 
 |-  ( i = ( `' g ` j ) -> ( f " ( ( iEdg ` A ) ` i ) ) = ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) )
22 2fveq3 
 |-  ( i = ( `' g ` j ) -> ( ( iEdg ` B ) ` ( g ` i ) ) = ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) )
23 21 22 eqeq12d 
 |-  ( i = ( `' g ` j ) -> ( ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) ) )
24 23 adantl 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) /\ i = ( `' g ` j ) ) -> ( ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) ) )
25 19 24 rspcdv 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) -> ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) ) )
26 f1ocnvfv2 
 |-  ( ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ j e. dom ( iEdg ` B ) ) -> ( g ` ( `' g ` j ) ) = j )
27 26 3ad2antl2 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( g ` ( `' g ` j ) ) = j )
28 27 fveq2d 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) )
29 28 eqeq2d 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) <-> ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) ) )
30 f1of1 
 |-  ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) -> f : ( Vtx ` A ) -1-1-> ( Vtx ` B ) )
31 30 3ad2ant3 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) -> f : ( Vtx ` A ) -1-1-> ( Vtx ` B ) )
32 31 adantr 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> f : ( Vtx ` A ) -1-1-> ( Vtx ` B ) )
33 simpl1l 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> A e. UHGraph )
34 1 3 uhgrss 
 |-  ( ( A e. UHGraph /\ ( `' g ` j ) e. dom ( iEdg ` A ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) C_ ( Vtx ` A ) )
35 33 19 34 syl2anc 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) C_ ( Vtx ` A ) )
36 32 35 jca 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( f : ( Vtx ` A ) -1-1-> ( Vtx ` B ) /\ ( ( iEdg ` A ) ` ( `' g ` j ) ) C_ ( Vtx ` A ) ) )
37 36 adantr 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) /\ ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) ) -> ( f : ( Vtx ` A ) -1-1-> ( Vtx ` B ) /\ ( ( iEdg ` A ) ` ( `' g ` j ) ) C_ ( Vtx ` A ) ) )
38 f1imacnv 
 |-  ( ( f : ( Vtx ` A ) -1-1-> ( Vtx ` B ) /\ ( ( iEdg ` A ) ` ( `' g ` j ) ) C_ ( Vtx ` A ) ) -> ( `' f " ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) )
39 37 38 syl 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) /\ ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) ) -> ( `' f " ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) )
40 imaeq2 
 |-  ( ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) -> ( `' f " ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) )
41 40 adantl 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) /\ ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) ) -> ( `' f " ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) )
42 39 41 eqtr3d 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) /\ ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) )
43 42 ex 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` j ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) )
44 29 43 sylbid 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( ( f " ( ( iEdg ` A ) ` ( `' g ` j ) ) ) = ( ( iEdg ` B ) ` ( g ` ( `' g ` j ) ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) )
45 25 44 syld 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) /\ j e. dom ( iEdg ` B ) ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) )
46 45 ex 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) -> ( j e. dom ( iEdg ` B ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) ) )
47 46 com23 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) -> ( j e. dom ( iEdg ` B ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) ) )
48 47 3exp 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) -> ( f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) -> ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) -> ( j e. dom ( iEdg ` B ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) ) ) ) )
49 48 com34 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( 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 ) -> ( j e. dom ( iEdg ` B ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) ) ) ) )
50 49 impd 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( ( 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 ) -> ( j e. dom ( iEdg ` B ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) ) ) ) )
51 50 3imp1 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) /\ j e. dom ( iEdg ` B ) ) -> ( ( iEdg ` A ) ` ( `' g ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) )
52 51 eqcomd 
 |-  ( ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) /\ j e. dom ( iEdg ` B ) ) -> ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) )
53 52 ralrimiva 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) -> A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) )
54 17 53 jca 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) -> ( `' g : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) ) )
55 f1oeq1 
 |-  ( h = `' g -> ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) <-> `' g : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) ) )
56 fveq1 
 |-  ( h = `' g -> ( h ` j ) = ( `' g ` j ) )
57 56 fveq2d 
 |-  ( h = `' g -> ( ( iEdg ` A ) ` ( h ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) )
58 57 eqeq2d 
 |-  ( h = `' g -> ( ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) <-> ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) ) )
59 58 ralbidv 
 |-  ( h = `' g -> ( A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) <-> A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) ) )
60 55 59 anbi12d 
 |-  ( h = `' g -> ( ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) <-> ( `' g : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( `' g ` j ) ) ) ) )
61 14 54 60 spcedv 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) -> E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) )
62 61 3exp 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( ( 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 ) -> E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
63 62 exlimdv 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( 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 ) -> E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
64 63 com23 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( 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. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
65 64 imp32 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) )
66 11 65 jca 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) )
67 f1oeq1 
 |-  ( e = `' f -> ( e : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) <-> `' f : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) ) )
68 imaeq1 
 |-  ( e = `' f -> ( e " ( ( iEdg ` B ) ` j ) ) = ( `' f " ( ( iEdg ` B ) ` j ) ) )
69 68 eqeq1d 
 |-  ( e = `' f -> ( ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) <-> ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) )
70 69 ralbidv 
 |-  ( e = `' f -> ( A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) <-> A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) )
71 70 anbi2d 
 |-  ( e = `' f -> ( ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) <-> ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) )
72 71 exbidv 
 |-  ( e = `' f -> ( E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) <-> E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) )
73 67 72 anbi12d 
 |-  ( e = `' f -> ( ( e : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) <-> ( `' f : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( `' f " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
74 8 66 73 spcedv 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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. e ( e : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) )
75 2 1 4 3 isomgr 
 |-  ( ( B e. Y /\ A e. UHGraph ) -> ( B IsomGr A <-> E. e ( e : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
76 75 ancoms 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( B IsomGr A <-> E. e ( e : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
77 76 adantr 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) ) ) ) -> ( B IsomGr A <-> E. e ( e : ( Vtx ` B ) -1-1-onto-> ( Vtx ` A ) /\ E. h ( h : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` A ) /\ A. j e. dom ( iEdg ` B ) ( e " ( ( iEdg ` B ) ` j ) ) = ( ( iEdg ` A ) ` ( h ` j ) ) ) ) ) )
78 74 77 mpbird 
 |-  ( ( ( A e. UHGraph /\ B e. Y ) /\ ( 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 ) ) ) ) ) -> B IsomGr A )
79 78 ex 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( ( 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 ) ) ) ) -> B IsomGr A ) )
80 79 exlimdv 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( 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 ) ) ) ) -> B IsomGr A ) )
81 5 80 sylbid 
 |-  ( ( A e. UHGraph /\ B e. Y ) -> ( A IsomGr B -> B IsomGr A ) )