Metamath Proof Explorer

Theorem isomgrtrlem

Description: Lemma for isomgrtr . (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtrlem 
|- ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) )

Proof

Step Hyp Ref Expression
1 imaco 
 |-  ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( v " ( f " ( ( iEdg ` A ) ` j ) ) )
2 1 a1i 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( v " ( f " ( ( iEdg ` A ) ` j ) ) ) )
3 fveq2 
 |-  ( i = j -> ( ( iEdg ` A ) ` i ) = ( ( iEdg ` A ) ` j ) )
4 3 imaeq2d 
 |-  ( i = j -> ( f " ( ( iEdg ` A ) ` i ) ) = ( f " ( ( iEdg ` A ) ` j ) ) )
5 2fveq3 
 |-  ( i = j -> ( ( iEdg ` B ) ` ( g ` i ) ) = ( ( iEdg ` B ) ` ( g ` j ) ) )
6 4 5 eqeq12d 
 |-  ( i = j -> ( ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) <-> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( g ` j ) ) ) )
7 6 rspccv 
 |-  ( A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) -> ( j e. dom ( iEdg ` A ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( g ` j ) ) ) )
8 7 adantl 
 |-  ( ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) -> ( j e. dom ( iEdg ` A ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( g ` j ) ) ) )
9 8 ad2antlr 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> ( j e. dom ( iEdg ` A ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( g ` j ) ) ) )
10 9 imp 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( f " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` B ) ` ( g ` j ) ) )
11 10 imaeq2d 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( v " ( f " ( ( iEdg ` A ) ` j ) ) ) = ( v " ( ( iEdg ` B ) ` ( g ` j ) ) ) )
12 simplrr 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) )
13 f1of 
 |-  ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) -> g : dom ( iEdg ` A ) --> dom ( iEdg ` B ) )
14 ffvelrn 
 |-  ( ( g : dom ( iEdg ` A ) --> dom ( iEdg ` B ) /\ j e. dom ( iEdg ` A ) ) -> ( g ` j ) e. dom ( iEdg ` B ) )
15 14 ex 
 |-  ( g : dom ( iEdg ` A ) --> dom ( iEdg ` B ) -> ( j e. dom ( iEdg ` A ) -> ( g ` j ) e. dom ( iEdg ` B ) ) )
16 13 15 syl 
 |-  ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) -> ( j e. dom ( iEdg ` A ) -> ( g ` j ) e. dom ( iEdg ` B ) ) )
17 16 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 ) ) ) -> ( j e. dom ( iEdg ` A ) -> ( g ` j ) e. dom ( iEdg ` B ) ) )
18 17 ad2antlr 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> ( j e. dom ( iEdg ` A ) -> ( g ` j ) e. dom ( iEdg ` B ) ) )
19 18 imp 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( g ` j ) e. dom ( iEdg ` B ) )
20 fveq2 
 |-  ( k = ( g ` j ) -> ( ( iEdg ` B ) ` k ) = ( ( iEdg ` B ) ` ( g ` j ) ) )
21 20 imaeq2d 
 |-  ( k = ( g ` j ) -> ( v " ( ( iEdg ` B ) ` k ) ) = ( v " ( ( iEdg ` B ) ` ( g ` j ) ) ) )
22 2fveq3 
 |-  ( k = ( g ` j ) -> ( ( iEdg ` C ) ` ( w ` k ) ) = ( ( iEdg ` C ) ` ( w ` ( g ` j ) ) ) )
23 21 22 eqeq12d 
 |-  ( k = ( g ` j ) -> ( ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) <-> ( v " ( ( iEdg ` B ) ` ( g ` j ) ) ) = ( ( iEdg ` C ) ` ( w ` ( g ` j ) ) ) ) )
24 23 rspccv 
 |-  ( A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) -> ( ( g ` j ) e. dom ( iEdg ` B ) -> ( v " ( ( iEdg ` B ) ` ( g ` j ) ) ) = ( ( iEdg ` C ) ` ( w ` ( g ` j ) ) ) ) )
25 12 19 24 sylc 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( v " ( ( iEdg ` B ) ` ( g ` j ) ) ) = ( ( iEdg ` C ) ` ( w ` ( g ` j ) ) ) )
26 11 25 eqtrd 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( v " ( f " ( ( iEdg ` A ) ` j ) ) ) = ( ( iEdg ` C ) ` ( w ` ( g ` j ) ) ) )
27 f1ofn 
 |-  ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) -> g Fn dom ( iEdg ` A ) )
28 27 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 Fn dom ( iEdg ` A ) )
29 28 ad2antlr 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> g Fn dom ( iEdg ` A ) )
30 fvco2 
 |-  ( ( g Fn dom ( iEdg ` A ) /\ j e. dom ( iEdg ` A ) ) -> ( ( w o. g ) ` j ) = ( w ` ( g ` j ) ) )
31 29 30 sylan 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( w o. g ) ` j ) = ( w ` ( g ` j ) ) )
32 31 eqcomd 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( w ` ( g ` j ) ) = ( ( w o. g ) ` j ) )
33 32 fveq2d 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( iEdg ` C ) ` ( w ` ( g ` j ) ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) )
34 2 26 33 3eqtrd 
 |-  ( ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) /\ j e. dom ( iEdg ` A ) ) -> ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) )
35 34 ralrimiva 
 |-  ( ( ( ( ( A e. UHGraph /\ B e. UHGraph /\ C e. X ) /\ f : ( Vtx ` A ) -1-1-onto-> ( Vtx ` B ) /\ v : ( Vtx ` B ) -1-1-onto-> ( Vtx ` C ) ) /\ ( g : dom ( iEdg ` A ) -1-1-onto-> dom ( iEdg ` B ) /\ A. i e. dom ( iEdg ` A ) ( f " ( ( iEdg ` A ) ` i ) ) = ( ( iEdg ` B ) ` ( g ` i ) ) ) ) /\ ( w : dom ( iEdg ` B ) -1-1-onto-> dom ( iEdg ` C ) /\ A. k e. dom ( iEdg ` B ) ( v " ( ( iEdg ` B ) ` k ) ) = ( ( iEdg ` C ) ` ( w ` k ) ) ) ) -> A. j e. dom ( iEdg ` A ) ( ( v o. f ) " ( ( iEdg ` A ) ` j ) ) = ( ( iEdg ` C ) ` ( ( w o. g ) ` j ) ) )