Metamath Proof Explorer

Theorem uhgrimisgrgric

Description: For isomorphic hypergraphs, the induced subgraph of a subset of vertices of one graph is isomorphic to the subgraph induced by the image of the subset. (Contributed by AV, 31-May-2025)

Ref Expression
Hypothesis uhgrimisgrgric.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion uhgrimisgrgric ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 uhgrimisgrgric.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grimdmrel ⊢ Rel dom GraphIso
3 2 ovrcl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
4 3 3ad2ant2 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
5 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
6 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
7 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
8 1 5 6 7 grimprop ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
9 f1ofun ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → Fun 𝐹 )
10 9 3ad2ant1 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → Fun 𝐹 )
11 1 fvexi ⊢ 𝑉 ∈ V
12 11 ssex ⊢ ( 𝑁 ⊆ 𝑉 → 𝑁 ∈ V )
13 resfunexg ⊢ ( ( Fun 𝐹 ∧ 𝑁 ∈ V ) → ( 𝐹 ↾ 𝑁 ) ∈ V )
14 10 12 13 syl2an ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐹 ↾ 𝑁 ) ∈ V )
15 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) )
16 15 3ad2ant1 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) )
17 f1ores ⊢ ( ( 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) )
18 16 17 sylan ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) )
19 simpr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) )
20 vex ⊢ 𝑔 ∈ V
21 20 resex ⊢ ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∈ V
22 21 a1i ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∈ V )
23 f1of1 ⊢ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1→ dom ( iEdg ‘ 𝐻 ) )
24 23 adantr ⊢ ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1→ dom ( iEdg ‘ 𝐻 ) )
25 24 3ad2ant2 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1→ dom ( iEdg ‘ 𝐻 ) )
26 25 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1→ dom ( iEdg ‘ 𝐻 ) )
27 ssrab2 ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 )
28 f1ores ⊢ ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1→ dom ( iEdg ‘ 𝐻 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) )
29 26 27 28 sylancl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) )
30 1 6 uhgrf ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
31 id ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
32 difssd ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝒫 𝑉 ∖ { ∅ } ) ⊆ 𝒫 𝑉 )
33 31 32 fssd ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 )
34 30 33 syl ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 )
35 34 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 )
36 35 anim2i ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 ) )
37 36 3adant2 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 ) )
38 37 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 ) )
39 simp2l ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
40 39 anim1i ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) )
41 40 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) )
42 41 ancomd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑁 ⊆ 𝑉 ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) )
43 simpl2r ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
44 43 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
45 uhgrimisgrgriclem ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ 𝒫 𝑉 ) ∧ ( 𝑁 ⊆ 𝑉 ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝑔 ‘ 𝑘 ) = 𝑗 ) ) )
46 38 42 44 45 syl3anc ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝑔 ‘ 𝑘 ) = 𝑗 ) ) )
47 fveq2 ⊢ ( 𝑥 = 𝑘 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
48 47 sseq1d ⊢ ( 𝑥 = 𝑘 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑁 ) )
49 48 rexrab ⊢ ( ∃ 𝑘 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑔 ‘ 𝑘 ) = 𝑗 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑁 ∧ ( 𝑔 ‘ 𝑘 ) = 𝑗 ) )
50 46 49 bitr4di ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑗 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) ⊆ ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑘 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑔 ‘ 𝑘 ) = 𝑗 ) )
51 fveq2 ⊢ ( 𝑥 = 𝑗 → ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) )
52 51 sseq1d ⊢ ( 𝑥 = 𝑗 → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) ⊆ ( 𝐹 “ 𝑁 ) ) )
53 52 elrab ⊢ ( 𝑗 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ↔ ( 𝑗 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) ⊆ ( 𝐹 “ 𝑁 ) ) )
54 53 a1i ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑗 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ↔ ( 𝑗 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑗 ) ⊆ ( 𝐹 “ 𝑁 ) ) ) )
55 f1ofn ⊢ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑔 Fn dom ( iEdg ‘ 𝐺 ) )
56 55 27 jctir ⊢ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → ( 𝑔 Fn dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
57 56 adantr ⊢ ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝑔 Fn dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
58 57 3ad2ant2 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → ( 𝑔 Fn dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
59 58 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑔 Fn dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
60 fvelimab ⊢ ( ( 𝑔 Fn dom ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑗 ∈ ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ↔ ∃ 𝑘 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑔 ‘ 𝑘 ) = 𝑗 ) )
61 59 60 syl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑗 ∈ ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ↔ ∃ 𝑘 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑔 ‘ 𝑘 ) = 𝑗 ) )
62 50 54 61 3bitr4d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑗 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ↔ 𝑗 ∈ ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ) )
63 62 eqrdv ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } = ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) )
64 63 f1oeq3d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ↔ ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ ( 𝑔 “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ) )
65 29 64 mpbird ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } )
66 ssralv ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ⊆ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
67 27 66 ax-mp ⊢ ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
68 elex ⊢ ( 𝐺 ∈ UHGraph → 𝐺 ∈ V )
69 68 anim1i ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) )
70 69 3anim3i ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) )
71 70 anim1i ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) )
72 simpr ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
73 fvres ⊢ ( 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } → ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) )
74 73 ad2antlr ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) = ( 𝑔 ‘ 𝑖 ) )
75 74 fveq2d ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) )
76 fveq2 ⊢ ( 𝑥 = 𝑖 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
77 76 sseq1d ⊢ ( 𝑥 = 𝑖 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) )
78 77 elrab ⊢ ( 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ↔ ( 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 ) )
79 78 simprbi ⊢ ( 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 )
80 79 ad2antlr ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 )
81 resima2 ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑁 → ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
82 80 81 syl ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
83 72 75 82 3eqtr4rd ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) )
84 83 ex ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
85 71 84 sylanl1 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
86 85 ralimdva ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
87 67 86 syl5 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
88 87 expimpd ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
89 88 3exp1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝑁 ⊆ 𝑉 → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) ) ) ) )
90 89 com25 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝑁 ⊆ 𝑉 → ( ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) ) ) ) )
91 90 3imp1 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
92 91 imp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) )
93 65 92 jca ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
94 f1oeq1 ⊢ ( ℎ = ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ↔ ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ) )
95 fveq1 ⊢ ( ℎ = ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ℎ ‘ 𝑖 ) = ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) )
96 95 fveq2d ⊢ ( ℎ = ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) )
97 96 eqeq2d ⊢ ( ℎ = ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
98 97 ralbidv ⊢ ( ℎ = ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) )
99 94 98 anbi12d ⊢ ( ℎ = ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) → ( ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ↔ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( 𝑔 ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ) ‘ 𝑖 ) ) ) ) )
100 22 93 99 spcedv ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) )
101 19 100 jca ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) ∧ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) → ( ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
102 18 101 mpdan ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
103 f1oeq1 ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( 𝑓 : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ↔ ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ) )
104 imaeq1 ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
105 104 eqeq1d ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) )
106 105 ralbidv ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) )
107 106 anbi2d ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ↔ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
108 107 exbidv ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ↔ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
109 103 108 anbi12d ⊢ ( 𝑓 = ( 𝐹 ↾ 𝑁 ) → ( ( 𝑓 : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ↔ ( ( 𝐹 ↾ 𝑁 ) : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( ( 𝐹 ↾ 𝑁 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ) )
110 14 102 109 spcedv ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
111 simpl3 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) )
112 simpr ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → 𝑁 ⊆ 𝑉 )
113 f1of ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : 𝑉 ⟶ ( Vtx ‘ 𝐻 ) )
114 113 fimassd ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( 𝐹 “ 𝑁 ) ⊆ ( Vtx ‘ 𝐻 ) )
115 114 a1d ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( 𝑁 ⊆ 𝑉 → ( 𝐹 “ 𝑁 ) ⊆ ( Vtx ‘ 𝐻 ) ) )
116 115 3ad2ant1 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) → ( 𝑁 ⊆ 𝑉 → ( 𝐹 “ 𝑁 ) ⊆ ( Vtx ‘ 𝐻 ) ) )
117 116 imp ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐹 “ 𝑁 ) ⊆ ( Vtx ‘ 𝐻 ) )
118 eqid ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } = { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 }
119 eqid ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } = { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) }
120 1 5 6 7 118 119 isubgrgrim ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ∧ ( 𝑁 ⊆ 𝑉 ∧ ( 𝐹 “ 𝑁 ) ⊆ ( Vtx ‘ 𝐻 ) ) ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ) )
121 111 112 117 120 syl12anc ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ ( 𝐹 “ 𝑁 ) ∧ ∃ ℎ ( ℎ : { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } –1-1-onto→ { 𝑥 ∈ dom ( iEdg ‘ 𝐻 ) ∣ ( ( iEdg ‘ 𝐻 ) ‘ 𝑥 ) ⊆ ( 𝐹 “ 𝑁 ) } ∧ ∀ 𝑖 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑁 } ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ) )
122 110 121 mpbird ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) )
123 122 3exp1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝑁 ⊆ 𝑉 → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) ) )
124 123 exlimdv ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝑁 ⊆ 𝑉 → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) ) )
125 124 imp ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝑁 ⊆ 𝑉 → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) )
126 8 125 syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ V ) → ( 𝑁 ⊆ 𝑉 → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) )
127 126 expd ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐺 ∈ UHGraph → ( 𝐻 ∈ V → ( 𝑁 ⊆ 𝑉 → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) ) )
128 127 com12 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐻 ∈ V → ( 𝑁 ⊆ 𝑉 → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) ) )
129 128 com34 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝑁 ⊆ 𝑉 → ( 𝐻 ∈ V → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) ) ) )
130 129 3imp ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐻 ∈ V → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) )
131 130 adantld ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) → ( ( 𝐺 ∈ V ∧ 𝐻 ∈ V ) → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) ) )
132 4 131 mpd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝑁 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐹 “ 𝑁 ) ) )