Metamath Proof Explorer

Theorem grimcnv

Description: The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025)

Ref Expression
Assertion grimcnv 
|- ( S e. UHGraph -> ( F e. ( S GraphIso T ) -> `' F e. ( T GraphIso S ) ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
2 eqid 
 |-  ( Vtx ` T ) = ( Vtx ` T )
3 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
4 eqid 
 |-  ( iEdg ` T ) = ( iEdg ` T )
5 1 2 3 4 grimprop 
 |-  ( F e. ( S GraphIso T ) -> ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) )
6 5 adantl 
 |-  ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) -> ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) )
7 f1ocnv 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> `' F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` S ) )
8 7 ad2antrl 
 |-  ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) ) -> `' F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` S ) )
9 vex 
 |-  j e. _V
10 cnvexg 
 |-  ( j e. _V -> `' j e. _V )
11 9 10 mp1i 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> `' j e. _V )
12 f1ocnv 
 |-  ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> `' j : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) )
13 12 ad2antrl 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> `' j : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) )
14 f1ofo 
 |-  ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> j : dom ( iEdg ` S ) -onto-> dom ( iEdg ` T ) )
15 14 ad2antrl 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> j : dom ( iEdg ` S ) -onto-> dom ( iEdg ` T ) )
16 foelcdmi 
 |-  ( ( j : dom ( iEdg ` S ) -onto-> dom ( iEdg ` T ) /\ x e. dom ( iEdg ` T ) ) -> E. y e. dom ( iEdg ` S ) ( j ` y ) = x )
17 15 16 sylan 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) /\ x e. dom ( iEdg ` T ) ) -> E. y e. dom ( iEdg ` S ) ( j ` y ) = x )
18 2fveq3 
 |-  ( i = y -> ( ( iEdg ` T ) ` ( j ` i ) ) = ( ( iEdg ` T ) ` ( j ` y ) ) )
19 fveq2 
 |-  ( i = y -> ( ( iEdg ` S ) ` i ) = ( ( iEdg ` S ) ` y ) )
20 19 imaeq2d 
 |-  ( i = y -> ( F " ( ( iEdg ` S ) ` i ) ) = ( F " ( ( iEdg ` S ) ` y ) ) )
21 18 20 eqeq12d 
 |-  ( i = y -> ( ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) <-> ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) )
22 21 rspcv 
 |-  ( y e. dom ( iEdg ` S ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) )
23 22 adantl 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) )
24 f1ocnvfv1 
 |-  ( ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ y e. dom ( iEdg ` S ) ) -> ( `' j ` ( j ` y ) ) = y )
25 24 ad4ant23 
 |-  ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( `' j ` ( j ` y ) ) = y )
26 25 fveq2d 
 |-  ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( ( iEdg ` S ) ` y ) )
27 f1of1 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> F : ( Vtx ` S ) -1-1-> ( Vtx ` T ) )
28 27 ad2antlr 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> F : ( Vtx ` S ) -1-1-> ( Vtx ` T ) )
29 1 3 uhgrss 
 |-  ( ( S e. UHGraph /\ y e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) )
30 29 ad5ant15 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) )
31 f1imacnv 
 |-  ( ( F : ( Vtx ` S ) -1-1-> ( Vtx ` T ) /\ ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) ) -> ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) = ( ( iEdg ` S ) ` y ) )
32 28 30 31 syl2an2r 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) = ( ( iEdg ` S ) ` y ) )
33 32 eqcomd 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` y ) = ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) )
34 33 adantr 
 |-  ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( ( iEdg ` S ) ` y ) = ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) )
35 26 34 eqtrd 
 |-  ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) )
36 35 adantlr 
 |-  ( ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) )
37 simplr 
 |-  ( ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) )
38 37 eqcomd 
 |-  ( ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) = ( ( iEdg ` T ) ` ( j ` y ) ) )
39 38 imaeq2d 
 |-  ( ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( `' F " ( F " ( ( iEdg ` S ) ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) )
40 36 39 eqtrd 
 |-  ( ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) /\ ( j ` y ) e. dom ( iEdg ` T ) ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) )
41 40 ex 
 |-  ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) )
42 41 ex 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) ) )
43 23 42 syld 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) ) )
44 43 ex 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> ( y e. dom ( iEdg ` S ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) ) ) )
45 44 com23 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) ) ) )
46 45 impr 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) ) )
47 eleq1 
 |-  ( ( j ` y ) = x -> ( ( j ` y ) e. dom ( iEdg ` T ) <-> x e. dom ( iEdg ` T ) ) )
48 2fveq3 
 |-  ( ( j ` y ) = x -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( ( iEdg ` S ) ` ( `' j ` x ) ) )
49 fveq2 
 |-  ( ( j ` y ) = x -> ( ( iEdg ` T ) ` ( j ` y ) ) = ( ( iEdg ` T ) ` x ) )
50 49 imaeq2d 
 |-  ( ( j ` y ) = x -> ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) )
51 48 50 eqeq12d 
 |-  ( ( j ` y ) = x -> ( ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) <-> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
52 47 51 imbi12d 
 |-  ( ( j ` y ) = x -> ( ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) <-> ( x e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) )
53 52 imbi2d 
 |-  ( ( j ` y ) = x -> ( ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` ( j ` y ) ) ) = ( `' F " ( ( iEdg ` T ) ` ( j ` y ) ) ) ) ) <-> ( y e. dom ( iEdg ` S ) -> ( x e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) ) )
54 46 53 syl5ibcom 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> ( ( j ` y ) = x -> ( y e. dom ( iEdg ` S ) -> ( x e. dom ( iEdg ` T ) -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) ) )
55 54 com24 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> ( x e. dom ( iEdg ` T ) -> ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) = x -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) ) )
56 55 imp31 
 |-  ( ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) /\ x e. dom ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( j ` y ) = x -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
57 56 rexlimdva 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) /\ x e. dom ( iEdg ` T ) ) -> ( E. y e. dom ( iEdg ` S ) ( j ` y ) = x -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
58 17 57 mpd 
 |-  ( ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) /\ x e. dom ( iEdg ` T ) ) -> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) )
59 58 ralrimiva 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) )
60 13 59 jca 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> ( `' j : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
61 f1oeq1 
 |-  ( f = `' j -> ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) <-> `' j : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) ) )
62 fveq1 
 |-  ( f = `' j -> ( f ` x ) = ( `' j ` x ) )
63 62 fveqeq2d 
 |-  ( f = `' j -> ( ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) <-> ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
64 63 ralbidv 
 |-  ( f = `' j -> ( A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) <-> A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
65 61 64 anbi12d 
 |-  ( f = `' j -> ( ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) <-> ( `' j : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( `' j ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) )
66 11 60 65 spcedv 
 |-  ( ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) /\ ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) -> E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
67 66 ex 
 |-  ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) -> ( ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) -> E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) )
68 67 exlimdv 
 |-  ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) ) -> ( E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) -> E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) )
69 68 impr 
 |-  ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) ) -> E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) )
70 grimdmrel 
 |-  Rel dom GraphIso
71 70 ovrcl 
 |-  ( F e. ( S GraphIso T ) -> ( S e. _V /\ T e. _V ) )
72 71 simprd 
 |-  ( F e. ( S GraphIso T ) -> T e. _V )
73 71 simpld 
 |-  ( F e. ( S GraphIso T ) -> S e. _V )
74 cnvexg 
 |-  ( F e. ( S GraphIso T ) -> `' F e. _V )
75 2 1 4 3 isgrim 
 |-  ( ( T e. _V /\ S e. _V /\ `' F e. _V ) -> ( `' F e. ( T GraphIso S ) <-> ( `' F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` S ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) ) )
76 72 73 74 75 syl3anc 
 |-  ( F e. ( S GraphIso T ) -> ( `' F e. ( T GraphIso S ) <-> ( `' F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` S ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) ) )
77 76 ad2antlr 
 |-  ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) ) -> ( `' F e. ( T GraphIso S ) <-> ( `' F : ( Vtx ` T ) -1-1-onto-> ( Vtx ` S ) /\ E. f ( f : dom ( iEdg ` T ) -1-1-onto-> dom ( iEdg ` S ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` S ) ` ( f ` x ) ) = ( `' F " ( ( iEdg ` T ) ` x ) ) ) ) ) )
78 8 69 77 mpbir2and 
 |-  ( ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) /\ ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ E. j ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) ) ) -> `' F e. ( T GraphIso S ) )
79 6 78 mpdan 
 |-  ( ( S e. UHGraph /\ F e. ( S GraphIso T ) ) -> `' F e. ( T GraphIso S ) )
80 79 ex 
 |-  ( S e. UHGraph -> ( F e. ( S GraphIso T ) -> `' F e. ( T GraphIso S ) ) )