Metamath Proof Explorer

Theorem isuspgrim0lem

Description: An isomorphism of simple pseudographs is a bijection between their vertices which induces a bijection between their edges. (Contributed by AV, 21-Apr-2025)

Ref Expression
Hypotheses isusgrim.v 
|- V = ( Vtx ` G )
isusgrim.w 
|- W = ( Vtx ` H )
isusgrim.e 
|- E = ( Edg ` G )
isusgrim.d 
|- D = ( Edg ` H )
isuspgrim0lem.i 
|- I = ( iEdg ` G )
isuspgrim0lem.j 
|- J = ( iEdg ` H )
isuspgrim0lem.m 
|- M = ( x e. E |-> ( F " x ) )
isuspgrim0lem.n 
|- N = ( x e. dom I |-> ( `' J ` ( M ` ( I ` x ) ) ) )
Assertion isuspgrim0lem 
|- ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> ( N : dom I -1-1-onto-> dom J /\ A. i e. dom I ( J ` ( N ` i ) ) = ( F " ( I ` i ) ) ) )

Proof

Step Hyp Ref Expression
1 isusgrim.v 
 |-  V = ( Vtx ` G )
2 isusgrim.w 
 |-  W = ( Vtx ` H )
3 isusgrim.e 
 |-  E = ( Edg ` G )
4 isusgrim.d 
 |-  D = ( Edg ` H )
5 isuspgrim0lem.i 
 |-  I = ( iEdg ` G )
6 isuspgrim0lem.j 
 |-  J = ( iEdg ` H )
7 isuspgrim0lem.m 
 |-  M = ( x e. E |-> ( F " x ) )
8 isuspgrim0lem.n 
 |-  N = ( x e. dom I |-> ( `' J ` ( M ` ( I ` x ) ) ) )
9 6 uspgrf1oedg 
 |-  ( H e. USPGraph -> J : dom J -1-1-onto-> ( Edg ` H ) )
10 9 3ad2ant2 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
11 10 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
12 f1of 
 |-  ( M : E -1-1-onto-> D -> M : E --> D )
13 12 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> M : E --> D )
14 13 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ x e. dom I ) -> M : E --> D )
15 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
16 5 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
17 15 16 syl 
 |-  ( G e. USPGraph -> Fun I )
18 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
19 5 eqcomi 
 |-  ( iEdg ` G ) = I
20 19 rneqi 
 |-  ran ( iEdg ` G ) = ran I
21 3 18 20 3eqtri 
 |-  E = ran I
22 feq3 
 |-  ( E = ran I -> ( I : dom I --> E <-> I : dom I --> ran I ) )
23 21 22 ax-mp 
 |-  ( I : dom I --> E <-> I : dom I --> ran I )
24 fdmrn 
 |-  ( Fun I <-> I : dom I --> ran I )
25 23 24 bitr4i 
 |-  ( I : dom I --> E <-> Fun I )
26 17 25 sylibr 
 |-  ( G e. USPGraph -> I : dom I --> E )
27 26 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> I : dom I --> E )
28 27 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> I : dom I --> E )
29 28 ffvelcdmda 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ x e. dom I ) -> ( I ` x ) e. E )
30 14 29 ffvelcdmd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ x e. dom I ) -> ( M ` ( I ` x ) ) e. D )
31 30 4 eleqtrdi 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ x e. dom I ) -> ( M ` ( I ` x ) ) e. ( Edg ` H ) )
32 f1ocnvdm 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( M ` ( I ` x ) ) e. ( Edg ` H ) ) -> ( `' J ` ( M ` ( I ` x ) ) ) e. dom J )
33 11 31 32 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ x e. dom I ) -> ( `' J ` ( M ` ( I ` x ) ) ) e. dom J )
34 33 ralrimiva 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> A. x e. dom I ( `' J ` ( M ` ( I ` x ) ) ) e. dom J )
35 2fveq3 
 |-  ( x = ( `' I ` ( `' M ` ( J ` i ) ) ) -> ( M ` ( I ` x ) ) = ( M ` ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) ) )
36 35 eqeq2d 
 |-  ( x = ( `' I ` ( `' M ` ( J ` i ) ) ) -> ( ( J ` i ) = ( M ` ( I ` x ) ) <-> ( J ` i ) = ( M ` ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) ) ) )
37 5 uspgrf1oedg 
 |-  ( G e. USPGraph -> I : dom I -1-1-onto-> ( Edg ` G ) )
38 37 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> I : dom I -1-1-onto-> ( Edg ` G ) )
39 38 ad2antrr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> I : dom I -1-1-onto-> ( Edg ` G ) )
40 f1oeq2 
 |-  ( E = ( Edg ` G ) -> ( M : E -1-1-onto-> D <-> M : ( Edg ` G ) -1-1-onto-> D ) )
41 3 40 ax-mp 
 |-  ( M : E -1-1-onto-> D <-> M : ( Edg ` G ) -1-1-onto-> D )
42 41 biimpi 
 |-  ( M : E -1-1-onto-> D -> M : ( Edg ` G ) -1-1-onto-> D )
43 42 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> M : ( Edg ` G ) -1-1-onto-> D )
44 f1oeq3 
 |-  ( D = ( Edg ` H ) -> ( J : dom J -1-1-onto-> D <-> J : dom J -1-1-onto-> ( Edg ` H ) ) )
45 4 44 ax-mp 
 |-  ( J : dom J -1-1-onto-> D <-> J : dom J -1-1-onto-> ( Edg ` H ) )
46 11 45 sylibr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> J : dom J -1-1-onto-> D )
47 f1of 
 |-  ( J : dom J -1-1-onto-> D -> J : dom J --> D )
48 46 47 syl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> J : dom J --> D )
49 48 ffvelcdmda 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( J ` i ) e. D )
50 f1ocnvdm 
 |-  ( ( M : ( Edg ` G ) -1-1-onto-> D /\ ( J ` i ) e. D ) -> ( `' M ` ( J ` i ) ) e. ( Edg ` G ) )
51 43 49 50 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( `' M ` ( J ` i ) ) e. ( Edg ` G ) )
52 f1ocnvdm 
 |-  ( ( I : dom I -1-1-onto-> ( Edg ` G ) /\ ( `' M ` ( J ` i ) ) e. ( Edg ` G ) ) -> ( `' I ` ( `' M ` ( J ` i ) ) ) e. dom I )
53 39 51 52 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( `' I ` ( `' M ` ( J ` i ) ) ) e. dom I )
54 simpll1 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> G e. USPGraph )
55 54 37 syl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> I : dom I -1-1-onto-> ( Edg ` G ) )
56 simpr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> M : E -1-1-onto-> D )
57 f1ocnvdm 
 |-  ( ( M : E -1-1-onto-> D /\ ( J ` i ) e. D ) -> ( `' M ` ( J ` i ) ) e. E )
58 56 49 57 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( `' M ` ( J ` i ) ) e. E )
59 58 3 eleqtrdi 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( `' M ` ( J ` i ) ) e. ( Edg ` G ) )
60 f1ocnvfv2 
 |-  ( ( I : dom I -1-1-onto-> ( Edg ` G ) /\ ( `' M ` ( J ` i ) ) e. ( Edg ` G ) ) -> ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) = ( `' M ` ( J ` i ) ) )
61 55 59 60 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) = ( `' M ` ( J ` i ) ) )
62 61 fveq2d 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( M ` ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) ) = ( M ` ( `' M ` ( J ` i ) ) ) )
63 f1ocnvfv2 
 |-  ( ( M : E -1-1-onto-> D /\ ( J ` i ) e. D ) -> ( M ` ( `' M ` ( J ` i ) ) ) = ( J ` i ) )
64 56 49 63 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( M ` ( `' M ` ( J ` i ) ) ) = ( J ` i ) )
65 62 64 eqtr2d 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( J ` i ) = ( M ` ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) ) )
66 36 53 65 rspcedvdw 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> E. x e. dom I ( J ` i ) = ( M ` ( I ` x ) ) )
67 eqtr2 
 |-  ( ( ( J ` i ) = ( M ` ( I ` x ) ) /\ ( J ` i ) = ( M ` ( I ` y ) ) ) -> ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) )
68 f1of1 
 |-  ( M : E -1-1-onto-> D -> M : E -1-1-> D )
69 68 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> M : E -1-1-> D )
70 69 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> M : E -1-1-> D )
71 5 iedgedg 
 |-  ( ( Fun I /\ x e. dom I ) -> ( I ` x ) e. ( Edg ` G ) )
72 17 71 sylan 
 |-  ( ( G e. USPGraph /\ x e. dom I ) -> ( I ` x ) e. ( Edg ` G ) )
73 72 3 eleqtrrdi 
 |-  ( ( G e. USPGraph /\ x e. dom I ) -> ( I ` x ) e. E )
74 73 ex 
 |-  ( G e. USPGraph -> ( x e. dom I -> ( I ` x ) e. E ) )
75 5 iedgedg 
 |-  ( ( Fun I /\ y e. dom I ) -> ( I ` y ) e. ( Edg ` G ) )
76 17 75 sylan 
 |-  ( ( G e. USPGraph /\ y e. dom I ) -> ( I ` y ) e. ( Edg ` G ) )
77 76 3 eleqtrrdi 
 |-  ( ( G e. USPGraph /\ y e. dom I ) -> ( I ` y ) e. E )
78 77 ex 
 |-  ( G e. USPGraph -> ( y e. dom I -> ( I ` y ) e. E ) )
79 74 78 anim12d 
 |-  ( G e. USPGraph -> ( ( x e. dom I /\ y e. dom I ) -> ( ( I ` x ) e. E /\ ( I ` y ) e. E ) ) )
80 79 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> ( ( x e. dom I /\ y e. dom I ) -> ( ( I ` x ) e. E /\ ( I ` y ) e. E ) ) )
81 80 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( ( x e. dom I /\ y e. dom I ) -> ( ( I ` x ) e. E /\ ( I ` y ) e. E ) ) )
82 81 imp 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( I ` x ) e. E /\ ( I ` y ) e. E ) )
83 f1fveq 
 |-  ( ( M : E -1-1-> D /\ ( ( I ` x ) e. E /\ ( I ` y ) e. E ) ) -> ( ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) <-> ( I ` x ) = ( I ` y ) ) )
84 70 82 83 syl2an2r 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) <-> ( I ` x ) = ( I ` y ) ) )
85 f1of1 
 |-  ( I : dom I -1-1-onto-> ( Edg ` G ) -> I : dom I -1-1-> ( Edg ` G ) )
86 37 85 syl 
 |-  ( G e. USPGraph -> I : dom I -1-1-> ( Edg ` G ) )
87 86 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> I : dom I -1-1-> ( Edg ` G ) )
88 87 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> I : dom I -1-1-> ( Edg ` G ) )
89 f1veqaeq 
 |-  ( ( I : dom I -1-1-> ( Edg ` G ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) )
90 88 89 sylan 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) )
91 84 90 sylbid 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) -> x = y ) )
92 67 91 syl5 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( ( J ` i ) = ( M ` ( I ` x ) ) /\ ( J ` i ) = ( M ` ( I ` y ) ) ) -> x = y ) )
93 92 ralrimivva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> A. x e. dom I A. y e. dom I ( ( ( J ` i ) = ( M ` ( I ` x ) ) /\ ( J ` i ) = ( M ` ( I ` y ) ) ) -> x = y ) )
94 2fveq3 
 |-  ( x = y -> ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) )
95 94 eqeq2d 
 |-  ( x = y -> ( ( J ` i ) = ( M ` ( I ` x ) ) <-> ( J ` i ) = ( M ` ( I ` y ) ) ) )
96 95 reu4 
 |-  ( E! x e. dom I ( J ` i ) = ( M ` ( I ` x ) ) <-> ( E. x e. dom I ( J ` i ) = ( M ` ( I ` x ) ) /\ A. x e. dom I A. y e. dom I ( ( ( J ` i ) = ( M ` ( I ` x ) ) /\ ( J ` i ) = ( M ` ( I ` y ) ) ) -> x = y ) ) )
97 66 93 96 sylanbrc 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> E! x e. dom I ( J ` i ) = ( M ` ( I ` x ) ) )
98 10 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
99 13 ad2antrr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> M : E --> D )
100 27 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> I : dom I --> E )
101 100 ffvelcdmda 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( I ` x ) e. E )
102 99 101 ffvelcdmd 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( M ` ( I ` x ) ) e. D )
103 102 4 eleqtrdi 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( M ` ( I ` x ) ) e. ( Edg ` H ) )
104 f1ocnvfv2 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( M ` ( I ` x ) ) e. ( Edg ` H ) ) -> ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) = ( M ` ( I ` x ) ) )
105 98 103 104 syl2an2r 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) = ( M ` ( I ` x ) ) )
106 105 eqeq2d 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) <-> ( J ` i ) = ( M ` ( I ` x ) ) ) )
107 106 reubidva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( E! x e. dom I ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) <-> E! x e. dom I ( J ` i ) = ( M ` ( I ` x ) ) ) )
108 97 107 mpbird 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> E! x e. dom I ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) )
109 11 ad2antrr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> J : dom J -1-1-onto-> ( Edg ` H ) )
110 f1of1 
 |-  ( J : dom J -1-1-onto-> ( Edg ` H ) -> J : dom J -1-1-> ( Edg ` H ) )
111 109 110 syl 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> J : dom J -1-1-> ( Edg ` H ) )
112 simplr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> i e. dom J )
113 33 adantlr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( `' J ` ( M ` ( I ` x ) ) ) e. dom J )
114 f1fveq 
 |-  ( ( J : dom J -1-1-> ( Edg ` H ) /\ ( i e. dom J /\ ( `' J ` ( M ` ( I ` x ) ) ) e. dom J ) ) -> ( ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) <-> i = ( `' J ` ( M ` ( I ` x ) ) ) ) )
115 114 bicomd 
 |-  ( ( J : dom J -1-1-> ( Edg ` H ) /\ ( i e. dom J /\ ( `' J ` ( M ` ( I ` x ) ) ) e. dom J ) ) -> ( i = ( `' J ` ( M ` ( I ` x ) ) ) <-> ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) ) )
116 111 112 113 115 syl12anc 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) /\ x e. dom I ) -> ( i = ( `' J ` ( M ` ( I ` x ) ) ) <-> ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) ) )
117 116 reubidva 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> ( E! x e. dom I i = ( `' J ` ( M ` ( I ` x ) ) ) <-> E! x e. dom I ( J ` i ) = ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) ) )
118 108 117 mpbird 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom J ) -> E! x e. dom I i = ( `' J ` ( M ` ( I ` x ) ) ) )
119 118 ralrimiva 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> A. i e. dom J E! x e. dom I i = ( `' J ` ( M ` ( I ` x ) ) ) )
120 8 f1ompt 
 |-  ( N : dom I -1-1-onto-> dom J <-> ( A. x e. dom I ( `' J ` ( M ` ( I ` x ) ) ) e. dom J /\ A. i e. dom J E! x e. dom I i = ( `' J ` ( M ` ( I ` x ) ) ) ) )
121 34 119 120 sylanbrc 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> N : dom I -1-1-onto-> dom J )
122 2fveq3 
 |-  ( x = i -> ( M ` ( I ` x ) ) = ( M ` ( I ` i ) ) )
123 122 fveq2d 
 |-  ( x = i -> ( `' J ` ( M ` ( I ` x ) ) ) = ( `' J ` ( M ` ( I ` i ) ) ) )
124 123 adantl 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) /\ x = i ) -> ( `' J ` ( M ` ( I ` x ) ) ) = ( `' J ` ( M ` ( I ` i ) ) ) )
125 simpr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> i e. dom I )
126 fvexd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( `' J ` ( M ` ( I ` i ) ) ) e. _V )
127 8 124 125 126 fvmptd2 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( N ` i ) = ( `' J ` ( M ` ( I ` i ) ) ) )
128 127 fveq2d 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( J ` ( N ` i ) ) = ( J ` ( `' J ` ( M ` ( I ` i ) ) ) ) )
129 13 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> M : E --> D )
130 28 ffvelcdmda 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( I ` i ) e. E )
131 129 130 ffvelcdmd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( M ` ( I ` i ) ) e. D )
132 131 4 eleqtrdi 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( M ` ( I ` i ) ) e. ( Edg ` H ) )
133 f1ocnvfv2 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( M ` ( I ` i ) ) e. ( Edg ` H ) ) -> ( J ` ( `' J ` ( M ` ( I ` i ) ) ) ) = ( M ` ( I ` i ) ) )
134 11 132 133 syl2an2r 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( J ` ( `' J ` ( M ` ( I ` i ) ) ) ) = ( M ` ( I ` i ) ) )
135 simpr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) /\ x = ( I ` i ) ) -> x = ( I ` i ) )
136 135 imaeq2d 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) /\ x = ( I ` i ) ) -> ( F " x ) = ( F " ( I ` i ) ) )
137 simp3 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> F e. X )
138 137 ad3antrrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> F e. X )
139 138 imaexd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( F " ( I ` i ) ) e. _V )
140 7 136 130 139 fvmptd2 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( M ` ( I ` i ) ) = ( F " ( I ` i ) ) )
141 128 134 140 3eqtrd 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) /\ i e. dom I ) -> ( J ` ( N ` i ) ) = ( F " ( I ` i ) ) )
142 141 ralrimiva 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> A. i e. dom I ( J ` ( N ` i ) ) = ( F " ( I ` i ) ) )
143 121 142 jca 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) /\ F : V -1-1-onto-> W ) /\ M : E -1-1-onto-> D ) -> ( N : dom I -1-1-onto-> dom J /\ A. i e. dom I ( J ` ( N ` i ) ) = ( F " ( I ` i ) ) ) )