This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgrgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
isubgrgrim.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
isubgrgrim.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
isubgrgrim.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
isubgrgrim.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
Assertion isubgrgrim ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isubgrgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgrgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 isubgrgrim.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
4 isubgrgrim.j ⊢ 𝐽 = ( iEdg ‘ 𝐻 )
5 isubgrgrim.k ⊢ 𝐾 = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 }
6 isubgrgrim.l ⊢ 𝐿 = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 }
7 ovex ⊢ ( 𝐺 ISubGr 𝑁 ) ∈ V
8 ovex ⊢ ( 𝐻 ISubGr 𝑀 ) ∈ V
9 7 8 pm3.2i ⊢ ( ( 𝐺 ISubGr 𝑁 ) ∈ V ∧ ( 𝐻 ISubGr 𝑀 ) ∈ V )
10 eqid ⊢ ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) = ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) )
11 eqid ⊢ ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) = ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) )
12 eqid ⊢ ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) = ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) )
13 eqid ⊢ ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) = ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) )
14 10 11 12 13 dfgric2 ⊢ ( ( ( 𝐺 ISubGr 𝑁 ) ∈ V ∧ ( 𝐻 ISubGr 𝑀 ) ∈ V ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
15 9 14 mp1i ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
16 eqidd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → 𝑓 = 𝑓 )
17 1 isubgrvtx ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 𝑁 ⊆ 𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) = 𝑁 )
18 17 ad2ant2r ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) = 𝑁 )
19 2 isubgrvtx ⊢ ( ( 𝐻 ∈ 𝑇 ∧ 𝑀 ⊆ 𝑊 ) → ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) = 𝑀 )
20 19 ad2ant2l ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) = 𝑀 )
21 16 18 20 f1oeq123d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) ↔ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) )
22 eqidd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → 𝑔 = 𝑔 )
23 1 3 isubgriedg ⊢ ( ( 𝐺 ∈ 𝑈 ∧ 𝑁 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) = ( 𝐼 ↾ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ) )
24 23 ad2ant2r ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) = ( 𝐼 ↾ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ) )
25 24 dmeqd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) = dom ( 𝐼 ↾ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ) )
26 ssrab2 ⊢ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom 𝐼
27 26 a1i ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom 𝐼 )
28 ssdmres ⊢ ( { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom 𝐼 ↔ dom ( 𝐼 ↾ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ) = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } )
29 27 28 sylib ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → dom ( 𝐼 ↾ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ) = { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } )
30 5 eqcomi ⊢ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } = 𝐾
31 30 a1i ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } = 𝐾 )
32 25 29 31 3eqtrd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) = 𝐾 )
33 2 4 isubgriedg ⊢ ( ( 𝐻 ∈ 𝑇 ∧ 𝑀 ⊆ 𝑊 ) → ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) = ( 𝐽 ↾ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ) )
34 33 ad2ant2l ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) = ( 𝐽 ↾ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ) )
35 34 dmeqd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) = dom ( 𝐽 ↾ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ) )
36 ssrab2 ⊢ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom 𝐽
37 36 a1i ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom 𝐽 )
38 ssdmres ⊢ ( { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ⊆ dom 𝐽 ↔ dom ( 𝐽 ↾ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ) = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } )
39 37 38 sylib ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → dom ( 𝐽 ↾ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ) = { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } )
40 6 eqcomi ⊢ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } = 𝐿
41 40 a1i ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } = 𝐿 )
42 35 39 41 3eqtrd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) = 𝐿 )
43 22 32 42 f1oeq123d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ↔ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) )
44 43 anbi1d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
45 31 reseq2d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( 𝐼 ↾ { 𝑥 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑥 ) ⊆ 𝑁 } ) = ( 𝐼 ↾ 𝐾 ) )
46 24 45 eqtrd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) = ( 𝐼 ↾ 𝐾 ) )
47 46 fveq1d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) = ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) )
48 47 imaeq2d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) )
49 40 reseq2i ⊢ ( 𝐽 ↾ { 𝑥 ∈ dom 𝐽 ∣ ( 𝐽 ‘ 𝑥 ) ⊆ 𝑀 } ) = ( 𝐽 ↾ 𝐿 )
50 34 49 eqtrdi ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) = ( 𝐽 ↾ 𝐿 ) )
51 50 fveq1d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) )
52 48 51 eqeq12d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
53 32 52 raleqbidv ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
54 53 adantr ⊢ ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
55 fvres ⊢ ( 𝑖 ∈ 𝐾 → ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) = ( 𝐼 ‘ 𝑖 ) )
56 55 adantl ⊢ ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑖 ∈ 𝐾 ) → ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) = ( 𝐼 ‘ 𝑖 ) )
57 56 imaeq2d ⊢ ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑖 ∈ 𝐾 ) → ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) )
58 57 adantlr ⊢ ( ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ∧ 𝑖 ∈ 𝐾 ) → ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) )
59 f1of ⊢ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → 𝑔 : 𝐾 ⟶ 𝐿 )
60 59 adantl ⊢ ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → 𝑔 : 𝐾 ⟶ 𝐿 )
61 60 ffvelcdmda ⊢ ( ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ∧ 𝑖 ∈ 𝐾 ) → ( 𝑔 ‘ 𝑖 ) ∈ 𝐿 )
62 61 fvresd ⊢ ( ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ∧ 𝑖 ∈ 𝐾 ) → ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) )
63 58 62 eqeq12d ⊢ ( ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) ∧ 𝑖 ∈ 𝐾 ) → ( ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
64 63 ralbidva ⊢ ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → ( ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( ( 𝐼 ↾ 𝐾 ) ‘ 𝑖 ) ) = ( ( 𝐽 ↾ 𝐿 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
65 54 64 bitrd ⊢ ( ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
66 65 pm5.32da ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
67 44 66 bitrd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
68 67 exbidv ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
69 21 68 anbi12d ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
70 69 exbidv ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ ( Vtx ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) –1-1-onto→ dom ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ( 𝑓 “ ( ( iEdg ‘ ( 𝐺 ISubGr 𝑁 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ ( 𝐻 ISubGr 𝑀 ) ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
71 15 70 bitrd ⊢ ( ( ( 𝐺 ∈ 𝑈 ∧ 𝐻 ∈ 𝑇 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑀 ⊆ 𝑊 ) ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr 𝑀 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ∃ 𝑔 ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ∀ 𝑖 ∈ 𝐾 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )