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 bilani 
 |-  ( ( ( ( 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 )
43 f1oeq3 
 |-  ( D = ( Edg ` H ) -> ( J : dom J -1-1-onto-> D <-> J : dom J -1-1-onto-> ( Edg ` H ) ) )
44 4 43 ax-mp 
 |-  ( J : dom J -1-1-onto-> D <-> J : dom J -1-1-onto-> ( Edg ` H ) )
45 11 44 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 )
46 f1of 
 |-  ( J : dom J -1-1-onto-> D -> J : dom J --> D )
47 45 46 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 )
48 47 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 )
49 f1ocnvdm 
 |-  ( ( M : ( Edg ` G ) -1-1-onto-> D /\ ( J ` i ) e. D ) -> ( `' M ` ( J ` i ) ) e. ( Edg ` G ) )
50 42 48 49 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 ) )
51 f1ocnvdm 
 |-  ( ( I : dom I -1-1-onto-> ( Edg ` G ) /\ ( `' M ` ( J ` i ) ) e. ( Edg ` G ) ) -> ( `' I ` ( `' M ` ( J ` i ) ) ) e. dom I )
52 39 50 51 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 )
53 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 )
54 53 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 ) )
55 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 )
56 f1ocnvdm 
 |-  ( ( M : E -1-1-onto-> D /\ ( J ` i ) e. D ) -> ( `' M ` ( J ` i ) ) e. E )
57 55 48 56 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 )
58 57 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 ) )
59 f1ocnvfv2 
 |-  ( ( I : dom I -1-1-onto-> ( Edg ` G ) /\ ( `' M ` ( J ` i ) ) e. ( Edg ` G ) ) -> ( I ` ( `' I ` ( `' M ` ( J ` i ) ) ) ) = ( `' M ` ( J ` i ) ) )
60 54 58 59 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 ) ) )
61 60 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 ) ) ) )
62 f1ocnvfv2 
 |-  ( ( M : E -1-1-onto-> D /\ ( J ` i ) e. D ) -> ( M ` ( `' M ` ( J ` i ) ) ) = ( J ` i ) )
63 55 48 62 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 ) )
64 61 63 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 ) ) ) ) ) )
65 36 52 64 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 ) ) )
66 eqtr2 
 |-  ( ( ( J ` i ) = ( M ` ( I ` x ) ) /\ ( J ` i ) = ( M ` ( I ` y ) ) ) -> ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) )
67 f1of1 
 |-  ( M : E -1-1-onto-> D -> M : E -1-1-> D )
68 67 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 )
69 68 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 )
70 5 iedgedg 
 |-  ( ( Fun I /\ x e. dom I ) -> ( I ` x ) e. ( Edg ` G ) )
71 17 70 sylan 
 |-  ( ( G e. USPGraph /\ x e. dom I ) -> ( I ` x ) e. ( Edg ` G ) )
72 71 3 eleqtrrdi 
 |-  ( ( G e. USPGraph /\ x e. dom I ) -> ( I ` x ) e. E )
73 72 ex 
 |-  ( G e. USPGraph -> ( x e. dom I -> ( I ` x ) e. E ) )
74 5 iedgedg 
 |-  ( ( Fun I /\ y e. dom I ) -> ( I ` y ) e. ( Edg ` G ) )
75 17 74 sylan 
 |-  ( ( G e. USPGraph /\ y e. dom I ) -> ( I ` y ) e. ( Edg ` G ) )
76 75 3 eleqtrrdi 
 |-  ( ( G e. USPGraph /\ y e. dom I ) -> ( I ` y ) e. E )
77 76 ex 
 |-  ( G e. USPGraph -> ( y e. dom I -> ( I ` y ) e. E ) )
78 73 77 anim12d 
 |-  ( G e. USPGraph -> ( ( x e. dom I /\ y e. dom I ) -> ( ( I ` x ) e. E /\ ( I ` y ) e. E ) ) )
79 78 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 ) ) )
80 79 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 ) ) )
81 80 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 ) )
82 f1fveq 
 |-  ( ( M : E -1-1-> D /\ ( ( I ` x ) e. E /\ ( I ` y ) e. E ) ) -> ( ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) <-> ( I ` x ) = ( I ` y ) ) )
83 69 81 82 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 ) ) )
84 f1of1 
 |-  ( I : dom I -1-1-onto-> ( Edg ` G ) -> I : dom I -1-1-> ( Edg ` G ) )
85 37 84 syl 
 |-  ( G e. USPGraph -> I : dom I -1-1-> ( Edg ` G ) )
86 85 3ad2ant1 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> I : dom I -1-1-> ( Edg ` G ) )
87 86 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 ) )
88 f1veqaeq 
 |-  ( ( I : dom I -1-1-> ( Edg ` G ) /\ ( x e. dom I /\ y e. dom I ) ) -> ( ( I ` x ) = ( I ` y ) -> x = y ) )
89 87 88 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 ) )
90 83 89 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 ) )
91 66 90 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 ) )
92 91 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 ) )
93 2fveq3 
 |-  ( x = y -> ( M ` ( I ` x ) ) = ( M ` ( I ` y ) ) )
94 93 eqeq2d 
 |-  ( x = y -> ( ( J ` i ) = ( M ` ( I ` x ) ) <-> ( J ` i ) = ( M ` ( I ` y ) ) ) )
95 94 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 ) ) )
96 65 92 95 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 ) ) )
97 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 ) )
98 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 )
99 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 )
100 99 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 )
101 98 100 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 )
102 101 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 ) )
103 f1ocnvfv2 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( M ` ( I ` x ) ) e. ( Edg ` H ) ) -> ( J ` ( `' J ` ( M ` ( I ` x ) ) ) ) = ( M ` ( I ` x ) ) )
104 97 102 103 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 ) ) )
105 104 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 ) ) ) )
106 105 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 ) ) ) )
107 96 106 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 ) ) ) ) )
108 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 ) )
109 f1of1 
 |-  ( J : dom J -1-1-onto-> ( Edg ` H ) -> J : dom J -1-1-> ( Edg ` H ) )
110 108 109 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 ) )
111 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 )
112 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 )
113 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 ) ) ) ) )
114 113 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 ) ) ) ) ) )
115 110 111 112 114 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 ) ) ) ) ) )
116 115 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 ) ) ) ) ) )
117 107 116 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 ) ) ) )
118 117 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 ) ) ) )
119 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 ) ) ) ) )
120 34 118 119 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 )
121 2fveq3 
 |-  ( x = i -> ( M ` ( I ` x ) ) = ( M ` ( I ` i ) ) )
122 121 fveq2d 
 |-  ( x = i -> ( `' J ` ( M ` ( I ` x ) ) ) = ( `' J ` ( M ` ( I ` i ) ) ) )
123 122 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 ) ) ) )
124 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 )
125 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 )
126 8 123 124 125 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 ) ) ) )
127 126 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 ) ) ) ) )
128 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 )
129 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 )
130 128 129 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 )
131 130 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 ) )
132 f1ocnvfv2 
 |-  ( ( J : dom J -1-1-onto-> ( Edg ` H ) /\ ( M ` ( I ` i ) ) e. ( Edg ` H ) ) -> ( J ` ( `' J ` ( M ` ( I ` i ) ) ) ) = ( M ` ( I ` i ) ) )
133 11 131 132 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 ) ) )
134 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 ) )
135 134 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 ) ) )
136 simp3 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. X ) -> F e. X )
137 136 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 )
138 137 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 )
139 7 135 129 138 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 ) ) )
140 127 133 139 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 ) ) )
141 140 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 ) ) )
142 120 141 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 ) ) ) )