Metamath Proof Explorer

Theorem grimuhgr

Description: If there is a graph isomorphism between a hypergraph and a class with an edge function, the class is also a hypergraph. (Contributed by AV, 2-May-2025)

Ref Expression
Assertion grimuhgr 
|- ( ( S e. UHGraph /\ F e. ( S GraphIso T ) /\ Fun ( iEdg ` T ) ) -> T e. UHGraph )

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 fdmrn 
 |-  ( Fun ( iEdg ` T ) <-> ( iEdg ` T ) : dom ( iEdg ` T ) --> ran ( iEdg ` T ) )
7 6 biimpi 
 |-  ( Fun ( iEdg ` T ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ran ( iEdg ` T ) )
8 7 3ad2ant3 
 |-  ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ran ( iEdg ` T ) )
9 8 adantr 
 |-  ( ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ran ( iEdg ` T ) )
10 funfn 
 |-  ( Fun ( iEdg ` T ) <-> ( iEdg ` T ) Fn dom ( iEdg ` T ) )
11 10 biimpi 
 |-  ( Fun ( iEdg ` T ) -> ( iEdg ` T ) Fn dom ( iEdg ` T ) )
12 11 3ad2ant3 
 |-  ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) -> ( iEdg ` T ) Fn dom ( iEdg ` T ) )
13 f1ofo 
 |-  ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> j : dom ( iEdg ` S ) -onto-> dom ( iEdg ` T ) )
14 13 3ad2ant2 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> j : dom ( iEdg ` S ) -onto-> dom ( iEdg ` T ) )
15 14 3ad2ant1 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( 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 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( 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 17 ex 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( 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 ) )
19 2fveq3 
 |-  ( i = y -> ( ( iEdg ` T ) ` ( j ` i ) ) = ( ( iEdg ` T ) ` ( j ` y ) ) )
20 fveq2 
 |-  ( i = y -> ( ( iEdg ` S ) ` i ) = ( ( iEdg ` S ) ` y ) )
21 20 imaeq2d 
 |-  ( i = y -> ( F " ( ( iEdg ` S ) ` i ) ) = ( F " ( ( iEdg ` S ) ` y ) ) )
22 19 21 eqeq12d 
 |-  ( i = y -> ( ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) <-> ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) )
23 22 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 ) ) ) )
24 23 adantl 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( 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 ) ) ) )
25 f1ofun 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> Fun F )
26 25 3ad2ant1 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> Fun F )
27 26 adantr 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) -> Fun F )
28 fvex 
 |-  ( ( iEdg ` S ) ` y ) e. _V
29 28 a1i 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` y ) e. _V )
30 funimaexg 
 |-  ( ( Fun F /\ ( ( iEdg ` S ) ` y ) e. _V ) -> ( F " ( ( iEdg ` S ) ` y ) ) e. _V )
31 27 29 30 syl2an2r 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) e. _V )
32 f1of 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> F : ( Vtx ` S ) --> ( Vtx ` T ) )
33 32 fimassd 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> ( F " ( ( iEdg ` S ) ` y ) ) C_ ( Vtx ` T ) )
34 33 3ad2ant1 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) C_ ( Vtx ` T ) )
35 34 adantr 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) C_ ( Vtx ` T ) )
36 35 adantr 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) C_ ( Vtx ` T ) )
37 31 36 elpwd 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) e. ~P ( Vtx ` T ) )
38 f1odm 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> dom F = ( Vtx ` S ) )
39 38 adantr 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> dom F = ( Vtx ` S ) )
40 39 adantr 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ y e. dom ( iEdg ` S ) ) -> dom F = ( Vtx ` S ) )
41 40 ineq1d 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ y e. dom ( iEdg ` S ) ) -> ( dom F i^i ( ( iEdg ` S ) ` y ) ) = ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) )
42 ffvelcdm 
 |-  ( ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) /\ y e. dom ( iEdg ` S ) ) -> ( ( iEdg ` S ) ` y ) e. ( ~P ( Vtx ` S ) \ { (/) } ) )
43 42 ex 
 |-  ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( y e. dom ( iEdg ` S ) -> ( ( iEdg ` S ) ` y ) e. ( ~P ( Vtx ` S ) \ { (/) } ) ) )
44 43 adantl 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( iEdg ` S ) ` y ) e. ( ~P ( Vtx ` S ) \ { (/) } ) ) )
45 eldifsn 
 |-  ( ( ( iEdg ` S ) ` y ) e. ( ~P ( Vtx ` S ) \ { (/) } ) <-> ( ( ( iEdg ` S ) ` y ) e. ~P ( Vtx ` S ) /\ ( ( iEdg ` S ) ` y ) =/= (/) ) )
46 28 elpw 
 |-  ( ( ( iEdg ` S ) ` y ) e. ~P ( Vtx ` S ) <-> ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) )
47 45 46 bianbi 
 |-  ( ( ( iEdg ` S ) ` y ) e. ( ~P ( Vtx ` S ) \ { (/) } ) <-> ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) /\ ( ( iEdg ` S ) ` y ) =/= (/) ) )
48 sseqin2 
 |-  ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) <-> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) = ( ( iEdg ` S ) ` y ) )
49 48 biimpi 
 |-  ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) = ( ( iEdg ` S ) ` y ) )
50 49 adantr 
 |-  ( ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) /\ ( ( iEdg ` S ) ` y ) =/= (/) ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) = ( ( iEdg ` S ) ` y ) )
51 simpr 
 |-  ( ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) /\ ( ( iEdg ` S ) ` y ) =/= (/) ) -> ( ( iEdg ` S ) ` y ) =/= (/) )
52 50 51 eqnetrd 
 |-  ( ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) /\ ( ( iEdg ` S ) ` y ) =/= (/) ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) =/= (/) )
53 52 a1i 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( ( ( ( iEdg ` S ) ` y ) C_ ( Vtx ` S ) /\ ( ( iEdg ` S ) ` y ) =/= (/) ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
54 47 53 biimtrid 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( ( ( iEdg ` S ) ` y ) e. ( ~P ( Vtx ` S ) \ { (/) } ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
55 44 54 syld 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
56 55 imp 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( Vtx ` S ) i^i ( ( iEdg ` S ) ` y ) ) =/= (/) )
57 41 56 eqnetrd 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ y e. dom ( iEdg ` S ) ) -> ( dom F i^i ( ( iEdg ` S ) ` y ) ) =/= (/) )
58 57 ex 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( y e. dom ( iEdg ` S ) -> ( dom F i^i ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
59 58 3adant2 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( y e. dom ( iEdg ` S ) -> ( dom F i^i ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
60 59 adantr 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) -> ( y e. dom ( iEdg ` S ) -> ( dom F i^i ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
61 60 imp 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( dom F i^i ( ( iEdg ` S ) ` y ) ) =/= (/) )
62 61 imadisjlnd 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) =/= (/) )
63 eldifsn 
 |-  ( ( F " ( ( iEdg ` S ) ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) <-> ( ( F " ( ( iEdg ` S ) ` y ) ) e. ~P ( Vtx ` T ) /\ ( F " ( ( iEdg ` S ) ` y ) ) =/= (/) ) )
64 37 62 63 sylanbrc 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) )
65 64 adantr 
 |-  ( ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) -> ( F " ( ( iEdg ` S ) ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) )
66 eleq1 
 |-  ( ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) -> ( ( ( iEdg ` T ) ` ( j ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) <-> ( F " ( ( iEdg ` S ) ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
67 66 adantl 
 |-  ( ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) -> ( ( ( iEdg ` T ) ` ( j ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) <-> ( F " ( ( iEdg ` S ) ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
68 65 67 mpbird 
 |-  ( ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) -> ( ( iEdg ` T ) ` ( j ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) )
69 fveq2 
 |-  ( ( j ` y ) = x -> ( ( iEdg ` T ) ` ( j ` y ) ) = ( ( iEdg ` T ) ` x ) )
70 69 eleq1d 
 |-  ( ( j ` y ) = x -> ( ( ( iEdg ` T ) ` ( j ` y ) ) e. ( ~P ( Vtx ` T ) \ { (/) } ) <-> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
71 68 70 syl5ibcom 
 |-  ( ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) /\ ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
72 71 ex 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( ( ( iEdg ` T ) ` ( j ` y ) ) = ( F " ( ( iEdg ` S ) ` y ) ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
73 24 72 syld 
 |-  ( ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) /\ y e. dom ( iEdg ` S ) ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
74 73 ex 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) -> ( y e. dom ( iEdg ` S ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) )
75 74 com23 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) )
76 75 ex 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( Fun ( iEdg ` T ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) ) )
77 76 3imp 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) -> ( y e. dom ( iEdg ` S ) -> ( ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
78 77 rexlimdv 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) -> ( E. y e. dom ( iEdg ` S ) ( j ` y ) = x -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
79 18 78 syld 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) -> ( x e. dom ( iEdg ` T ) -> ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
80 79 ralrimiv 
 |-  ( ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) /\ Fun ( iEdg ` T ) /\ A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) )
81 80 3exp 
 |-  ( ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) /\ j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( Fun ( iEdg ` T ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
82 81 3exp 
 |-  ( F : ( Vtx ` S ) -1-1-onto-> ( Vtx ` T ) -> ( j : dom ( iEdg ` S ) -1-1-onto-> dom ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( Fun ( iEdg ` T ) -> ( A. i e. dom ( iEdg ` S ) ( ( iEdg ` T ) ` ( j ` i ) ) = ( F " ( ( iEdg ` S ) ` i ) ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) ) )
83 82 com35 
 |-  ( 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 ) ) -> ( Fun ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) ) )
84 83 impd 
 |-  ( 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 ) ) ) -> ( Fun ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) )
85 84 3imp 
 |-  ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) )
86 85 imp 
 |-  ( ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) )
87 fnfvrnss 
 |-  ( ( ( iEdg ` T ) Fn dom ( iEdg ` T ) /\ A. x e. dom ( iEdg ` T ) ( ( iEdg ` T ) ` x ) e. ( ~P ( Vtx ` T ) \ { (/) } ) ) -> ran ( iEdg ` T ) C_ ( ~P ( Vtx ` T ) \ { (/) } ) )
88 12 86 87 syl2an2r 
 |-  ( ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ran ( iEdg ` T ) C_ ( ~P ( Vtx ` T ) \ { (/) } ) )
89 9 88 fssd 
 |-  ( ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) /\ ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) )
90 89 ex 
 |-  ( ( 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 ) ) ) /\ Fun ( iEdg ` T ) ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) )
91 90 3exp 
 |-  ( 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 ) ) ) -> ( Fun ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) )
92 91 exlimdv 
 |-  ( 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 ) ) ) -> ( Fun ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) ) )
93 92 imp 
 |-  ( ( 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 ) ) ) ) -> ( Fun ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
94 5 93 syl 
 |-  ( F e. ( S GraphIso T ) -> ( Fun ( iEdg ` T ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
95 94 impcom 
 |-  ( ( Fun ( iEdg ` T ) /\ F e. ( S GraphIso T ) ) -> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) )
96 grimdmrel 
 |-  Rel dom GraphIso
97 96 ovrcl 
 |-  ( F e. ( S GraphIso T ) -> ( S e. _V /\ T e. _V ) )
98 1 3 isuhgr 
 |-  ( S e. _V -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
99 98 adantr 
 |-  ( ( S e. _V /\ T e. _V ) -> ( S e. UHGraph <-> ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) ) )
100 2 4 isuhgr 
 |-  ( T e. _V -> ( T e. UHGraph <-> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) )
101 100 adantl 
 |-  ( ( S e. _V /\ T e. _V ) -> ( T e. UHGraph <-> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) )
102 99 101 imbi12d 
 |-  ( ( S e. _V /\ T e. _V ) -> ( ( S e. UHGraph -> T e. UHGraph ) <-> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
103 97 102 syl 
 |-  ( F e. ( S GraphIso T ) -> ( ( S e. UHGraph -> T e. UHGraph ) <-> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
104 103 adantl 
 |-  ( ( Fun ( iEdg ` T ) /\ F e. ( S GraphIso T ) ) -> ( ( S e. UHGraph -> T e. UHGraph ) <-> ( ( iEdg ` S ) : dom ( iEdg ` S ) --> ( ~P ( Vtx ` S ) \ { (/) } ) -> ( iEdg ` T ) : dom ( iEdg ` T ) --> ( ~P ( Vtx ` T ) \ { (/) } ) ) ) )
105 95 104 mpbird 
 |-  ( ( Fun ( iEdg ` T ) /\ F e. ( S GraphIso T ) ) -> ( S e. UHGraph -> T e. UHGraph ) )
106 105 ex 
 |-  ( Fun ( iEdg ` T ) -> ( F e. ( S GraphIso T ) -> ( S e. UHGraph -> T e. UHGraph ) ) )
107 106 3imp31 
 |-  ( ( S e. UHGraph /\ F e. ( S GraphIso T ) /\ Fun ( iEdg ` T ) ) -> T e. UHGraph )