Metamath Proof Explorer

Theorem isubgrgrim

Description: Isomorphic subgraphs induced by subsets of vertices of two graphs. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses isubgrgrim.v 
|- V = ( Vtx ` G )
isubgrgrim.w 
|- W = ( Vtx ` H )
isubgrgrim.i 
|- I = ( iEdg ` G )
isubgrgrim.j 
|- J = ( iEdg ` H )
isubgrgrim.k 
|- K = { x e. dom I | ( I ` x ) C_ N }
isubgrgrim.l 
|- L = { x e. dom J | ( J ` x ) C_ M }
Assertion isubgrgrim 
|- ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isubgrgrim.v 
 |-  V = ( Vtx ` G )
2 isubgrgrim.w 
 |-  W = ( Vtx ` H )
3 isubgrgrim.i 
 |-  I = ( iEdg ` G )
4 isubgrgrim.j 
 |-  J = ( iEdg ` H )
5 isubgrgrim.k 
 |-  K = { x e. dom I | ( I ` x ) C_ N }
6 isubgrgrim.l 
 |-  L = { x e. dom J | ( J ` x ) C_ M }
7 ovex 
 |-  ( G ISubGr N ) e. _V
8 ovex 
 |-  ( H ISubGr M ) e. _V
9 7 8 pm3.2i 
 |-  ( ( G ISubGr N ) e. _V /\ ( H ISubGr M ) e. _V )
10 eqid 
 |-  ( Vtx ` ( G ISubGr N ) ) = ( Vtx ` ( G ISubGr N ) )
11 eqid 
 |-  ( Vtx ` ( H ISubGr M ) ) = ( Vtx ` ( H ISubGr M ) )
12 eqid 
 |-  ( iEdg ` ( G ISubGr N ) ) = ( iEdg ` ( G ISubGr N ) )
13 eqid 
 |-  ( iEdg ` ( H ISubGr M ) ) = ( iEdg ` ( H ISubGr M ) )
14 10 11 12 13 dfgric2 
 |-  ( ( ( G ISubGr N ) e. _V /\ ( H ISubGr M ) e. _V ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : ( Vtx ` ( G ISubGr N ) ) -1-1-onto-> ( Vtx ` ( H ISubGr M ) ) /\ E. g ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) ) ) )
15 9 14 mp1i 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : ( Vtx ` ( G ISubGr N ) ) -1-1-onto-> ( Vtx ` ( H ISubGr M ) ) /\ E. g ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) ) ) )
16 eqidd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> f = f )
17 1 isubgrvtx 
 |-  ( ( G e. U /\ N C_ V ) -> ( Vtx ` ( G ISubGr N ) ) = N )
18 17 ad2ant2r 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( Vtx ` ( G ISubGr N ) ) = N )
19 2 isubgrvtx 
 |-  ( ( H e. T /\ M C_ W ) -> ( Vtx ` ( H ISubGr M ) ) = M )
20 19 ad2ant2l 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( Vtx ` ( H ISubGr M ) ) = M )
21 16 18 20 f1oeq123d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( f : ( Vtx ` ( G ISubGr N ) ) -1-1-onto-> ( Vtx ` ( H ISubGr M ) ) <-> f : N -1-1-onto-> M ) )
22 eqidd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> g = g )
23 1 3 isubgriedg 
 |-  ( ( G e. U /\ N C_ V ) -> ( iEdg ` ( G ISubGr N ) ) = ( I |` { x e. dom I | ( I ` x ) C_ N } ) )
24 23 ad2ant2r 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( iEdg ` ( G ISubGr N ) ) = ( I |` { x e. dom I | ( I ` x ) C_ N } ) )
25 24 dmeqd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> dom ( iEdg ` ( G ISubGr N ) ) = dom ( I |` { x e. dom I | ( I ` x ) C_ N } ) )
26 ssrab2 
 |-  { x e. dom I | ( I ` x ) C_ N } C_ dom I
27 26 a1i 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> { x e. dom I | ( I ` x ) C_ N } C_ dom I )
28 ssdmres 
 |-  ( { x e. dom I | ( I ` x ) C_ N } C_ dom I <-> dom ( I |` { x e. dom I | ( I ` x ) C_ N } ) = { x e. dom I | ( I ` x ) C_ N } )
29 27 28 sylib 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> dom ( I |` { x e. dom I | ( I ` x ) C_ N } ) = { x e. dom I | ( I ` x ) C_ N } )
30 5 eqcomi 
 |-  { x e. dom I | ( I ` x ) C_ N } = K
31 30 a1i 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> { x e. dom I | ( I ` x ) C_ N } = K )
32 25 29 31 3eqtrd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> dom ( iEdg ` ( G ISubGr N ) ) = K )
33 2 4 isubgriedg 
 |-  ( ( H e. T /\ M C_ W ) -> ( iEdg ` ( H ISubGr M ) ) = ( J |` { x e. dom J | ( J ` x ) C_ M } ) )
34 33 ad2ant2l 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( iEdg ` ( H ISubGr M ) ) = ( J |` { x e. dom J | ( J ` x ) C_ M } ) )
35 34 dmeqd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> dom ( iEdg ` ( H ISubGr M ) ) = dom ( J |` { x e. dom J | ( J ` x ) C_ M } ) )
36 ssrab2 
 |-  { x e. dom J | ( J ` x ) C_ M } C_ dom J
37 36 a1i 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> { x e. dom J | ( J ` x ) C_ M } C_ dom J )
38 ssdmres 
 |-  ( { x e. dom J | ( J ` x ) C_ M } C_ dom J <-> dom ( J |` { x e. dom J | ( J ` x ) C_ M } ) = { x e. dom J | ( J ` x ) C_ M } )
39 37 38 sylib 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> dom ( J |` { x e. dom J | ( J ` x ) C_ M } ) = { x e. dom J | ( J ` x ) C_ M } )
40 6 eqcomi 
 |-  { x e. dom J | ( J ` x ) C_ M } = L
41 40 a1i 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> { x e. dom J | ( J ` x ) C_ M } = L )
42 35 39 41 3eqtrd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> dom ( iEdg ` ( H ISubGr M ) ) = L )
43 22 32 42 f1oeq123d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) <-> g : K -1-1-onto-> L ) )
44 43 anbi1d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) <-> ( g : K -1-1-onto-> L /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) ) )
45 31 reseq2d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( I |` { x e. dom I | ( I ` x ) C_ N } ) = ( I |` K ) )
46 24 45 eqtrd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( iEdg ` ( G ISubGr N ) ) = ( I |` K ) )
47 46 fveq1d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( iEdg ` ( G ISubGr N ) ) ` i ) = ( ( I |` K ) ` i ) )
48 47 imaeq2d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( f " ( ( I |` K ) ` i ) ) )
49 40 reseq2i 
 |-  ( J |` { x e. dom J | ( J ` x ) C_ M } ) = ( J |` L )
50 34 49 eqtrdi 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( iEdg ` ( H ISubGr M ) ) = ( J |` L ) )
51 50 fveq1d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) = ( ( J |` L ) ` ( g ` i ) ) )
52 48 51 eqeq12d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) <-> ( f " ( ( I |` K ) ` i ) ) = ( ( J |` L ) ` ( g ` i ) ) ) )
53 32 52 raleqbidv 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) <-> A. i e. K ( f " ( ( I |` K ) ` i ) ) = ( ( J |` L ) ` ( g ` i ) ) ) )
54 53 adantr 
 |-  ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) -> ( A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) <-> A. i e. K ( f " ( ( I |` K ) ` i ) ) = ( ( J |` L ) ` ( g ` i ) ) ) )
55 fvres 
 |-  ( i e. K -> ( ( I |` K ) ` i ) = ( I ` i ) )
56 55 adantl 
 |-  ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ i e. K ) -> ( ( I |` K ) ` i ) = ( I ` i ) )
57 56 imaeq2d 
 |-  ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ i e. K ) -> ( f " ( ( I |` K ) ` i ) ) = ( f " ( I ` i ) ) )
58 57 adantlr 
 |-  ( ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) /\ i e. K ) -> ( f " ( ( I |` K ) ` i ) ) = ( f " ( I ` i ) ) )
59 f1of 
 |-  ( g : K -1-1-onto-> L -> g : K --> L )
60 59 adantl 
 |-  ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) -> g : K --> L )
61 60 ffvelcdmda 
 |-  ( ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) /\ i e. K ) -> ( g ` i ) e. L )
62 61 fvresd 
 |-  ( ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) /\ i e. K ) -> ( ( J |` L ) ` ( g ` i ) ) = ( J ` ( g ` i ) ) )
63 58 62 eqeq12d 
 |-  ( ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) /\ i e. K ) -> ( ( f " ( ( I |` K ) ` i ) ) = ( ( J |` L ) ` ( g ` i ) ) <-> ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
64 63 ralbidva 
 |-  ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) -> ( A. i e. K ( f " ( ( I |` K ) ` i ) ) = ( ( J |` L ) ` ( g ` i ) ) <-> A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
65 54 64 bitrd 
 |-  ( ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) /\ g : K -1-1-onto-> L ) -> ( A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) <-> A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) )
66 65 pm5.32da 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( g : K -1-1-onto-> L /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) <-> ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
67 44 66 bitrd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) <-> ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
68 67 exbidv 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( E. g ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) <-> E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) )
69 21 68 anbi12d 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( f : ( Vtx ` ( G ISubGr N ) ) -1-1-onto-> ( Vtx ` ( H ISubGr M ) ) /\ E. g ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) ) <-> ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
70 69 exbidv 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( E. f ( f : ( Vtx ` ( G ISubGr N ) ) -1-1-onto-> ( Vtx ` ( H ISubGr M ) ) /\ E. g ( g : dom ( iEdg ` ( G ISubGr N ) ) -1-1-onto-> dom ( iEdg ` ( H ISubGr M ) ) /\ A. i e. dom ( iEdg ` ( G ISubGr N ) ) ( f " ( ( iEdg ` ( G ISubGr N ) ) ` i ) ) = ( ( iEdg ` ( H ISubGr M ) ) ` ( g ` i ) ) ) ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
71 15 70 bitrd 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ V /\ M C_ W ) ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )