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

Metamath Proof Explorer

Theorem grimedg

Description: For two isomorphic graphs, a set of vertices is an edge in one graph iff its image by a graph isomorphism is an edge of the other graph. (Contributed by AV, 7-Jun-2025)

Ref Expression
Hypotheses grimedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
grimedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
grimedg.e ⊢ 𝐸 = ( Edg ‘ 𝐻 )
Assertion grimedg ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )

Proof

Step Hyp Ref Expression
1 grimedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 grimedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
3 grimedg.e ⊢ 𝐸 = ( Edg ‘ 𝐻 )
4 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
7 1 4 5 6 grimprop ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
8 2 eleq2i ⊢ ( 𝐾 ∈ 𝐼 ↔ 𝐾 ∈ ( Edg ‘ 𝐺 ) )
9 5 uhgredgiedgb ⊢ ( 𝐺 ∈ UHGraph → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
10 9 ad2antll ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
11 8 10 bitrid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( 𝐾 ∈ 𝐼 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
12 2fveq3 ⊢ ( 𝑖 = 𝑘 → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) )
13 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
14 13 imaeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑖 = 𝑘 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
16 15 rspcv ⊢ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
17 16 adantl ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
18 6 uhgrfun ⊢ ( 𝐻 ∈ UHGraph → Fun ( iEdg ‘ 𝐻 ) )
19 18 ad2antrr ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → Fun ( iEdg ‘ 𝐻 ) )
20 f1of ⊢ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
21 20 ad2antll ⊢ ( ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
22 simplr ⊢ ( ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ) → 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) )
23 21 22 ffvelcdmd ⊢ ( ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ) → ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) )
24 6 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐻 ) ∧ ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐻 ) )
25 24 3 eleqtrrdi ⊢ ( ( Fun ( iEdg ‘ 𝐻 ) ∧ ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐸 )
26 19 23 25 syl2an2r ⊢ ( ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐸 )
27 eleq1 ⊢ ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) → ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐸 ) )
28 27 eqcoms ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐸 ) )
29 26 28 syl5ibrcom ⊢ ( ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) )
30 29 ex ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) ) )
31 30 com23 ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) ) )
32 17 31 syld ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) ) )
33 32 com13 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) ) )
34 33 impr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) )
35 34 impl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 )
36 35 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 )
37 imaeq2 ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
38 37 eleq1d ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) )
39 38 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐸 ) )
40 36 39 mpbird ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐸 )
41 1 5 uhgrss ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 )
42 41 ex ⊢ ( 𝐺 ∈ UHGraph → ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 ) )
43 42 ad2antll ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 ) )
44 43 imp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 )
45 44 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 )
46 sseq1 ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐾 ⊆ 𝑉 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 ) )
47 46 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐾 ⊆ 𝑉 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ⊆ 𝑉 ) )
48 45 47 mpbird ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → 𝐾 ⊆ 𝑉 )
49 40 48 jca ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) )
50 49 ex ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )
51 50 rexlimdva ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )
52 11 51 sylbid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( 𝐾 ∈ 𝐼 → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )
53 3 eleq2i ⊢ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ↔ ( 𝐹 “ 𝐾 ) ∈ ( Edg ‘ 𝐻 ) )
54 6 uhgredgiedgb ⊢ ( 𝐻 ∈ UHGraph → ( ( 𝐹 “ 𝐾 ) ∈ ( Edg ‘ 𝐻 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
55 54 ad2antrl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( ( 𝐹 “ 𝐾 ) ∈ ( Edg ‘ 𝐻 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
56 53 55 bitrid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
57 f1ofo ⊢ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) –onto→ dom ( iEdg ‘ 𝐻 ) )
58 57 adantr ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) –onto→ dom ( iEdg ‘ 𝐻 ) )
59 58 ad2antlr ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) –onto→ dom ( iEdg ‘ 𝐻 ) )
60 foelrn ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) )
61 59 60 sylan ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) )
62 2fveq3 ⊢ ( 𝑖 = 𝑙 → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) )
63 fveq2 ⊢ ( 𝑖 = 𝑙 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) )
64 63 imaeq2d ⊢ ( 𝑖 = 𝑙 → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) )
65 62 64 eqeq12d ⊢ ( 𝑖 = 𝑙 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) )
66 65 rspcv ⊢ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) )
67 66 adantl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) )
68 fveq2 ⊢ ( 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) )
69 68 eqeq2d ⊢ ( 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ↔ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) )
70 69 ad2antll ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ↔ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) )
71 simpl ⊢ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) → 𝐻 ∈ UHGraph )
72 71 ad2antrl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) → 𝐻 ∈ UHGraph )
73 simplrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) )
74 eleq1 ⊢ ( 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ↔ ( 𝑗 ‘ 𝑙 ) ∈ dom ( iEdg ‘ 𝐻 ) ) )
75 74 ad2antll ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ↔ ( 𝑗 ‘ 𝑙 ) ∈ dom ( iEdg ‘ 𝐻 ) ) )
76 73 75 mpbid ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( 𝑗 ‘ 𝑙 ) ∈ dom ( iEdg ‘ 𝐻 ) )
77 4 6 uhgrss ⊢ ( ( 𝐻 ∈ UHGraph ∧ ( 𝑗 ‘ 𝑙 ) ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ⊆ ( Vtx ‘ 𝐻 ) )
78 72 76 77 syl2an2r ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ⊆ ( Vtx ‘ 𝐻 ) )
79 78 ad2antrr ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ⊆ ( Vtx ‘ 𝐻 ) )
80 sseq1 ⊢ ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) → ( ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ⊆ ( Vtx ‘ 𝐻 ) ) )
81 80 adantl ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ⊆ ( Vtx ‘ 𝐻 ) ) )
82 79 81 mpbird ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) → ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) )
83 eqeq2 ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ↔ ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) )
84 83 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ↔ ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) )
85 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) )
86 85 ad3antrrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) )
87 86 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) ∧ 𝐾 ⊆ 𝑉 ) → 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) )
88 simplr ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → 𝐺 ∈ UHGraph )
89 88 adantl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) → 𝐺 ∈ UHGraph )
90 simpl ⊢ ( ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) → 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) )
91 1 5 uhgrss ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ⊆ 𝑉 )
92 89 90 91 syl2an ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ⊆ 𝑉 )
93 92 ad2antrr ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ⊆ 𝑉 )
94 93 anim1ci ⊢ ( ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) ∧ 𝐾 ⊆ 𝑉 ) → ( 𝐾 ⊆ 𝑉 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ⊆ 𝑉 ) )
95 f1imaeq ⊢ ( ( 𝐹 : 𝑉 –1-1→ ( Vtx ‘ 𝐻 ) ∧ ( 𝐾 ⊆ 𝑉 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ⊆ 𝑉 ) ) → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ↔ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) )
96 87 94 95 syl2anc ⊢ ( ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) ∧ 𝐾 ⊆ 𝑉 ) → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ↔ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) )
97 5 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
98 97 ad2antlr ⊢ ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → Fun ( iEdg ‘ 𝐺 ) )
99 98 adantl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) → Fun ( iEdg ‘ 𝐺 ) )
100 5 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ∈ ( Edg ‘ 𝐺 ) )
101 99 90 100 syl2an ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ∈ ( Edg ‘ 𝐺 ) )
102 101 2 eleqtrrdi ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ∈ 𝐼 )
103 eleq1 ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) → ( 𝐾 ∈ 𝐼 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ∈ 𝐼 ) )
104 102 103 syl5ibrcom ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) → 𝐾 ∈ 𝐼 ) )
105 104 ad3antrrr ⊢ ( ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) ∧ 𝐾 ⊆ 𝑉 ) → ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) → 𝐾 ∈ 𝐼 ) )
106 96 105 sylbid ⊢ ( ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) ∧ 𝐾 ⊆ 𝑉 ) → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → 𝐾 ∈ 𝐼 ) )
107 106 ex ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) → ( 𝐾 ⊆ 𝑉 → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → 𝐾 ∈ 𝐼 ) ) )
108 107 com23 ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) )
109 108 ex ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
110 109 com23 ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
111 84 110 sylbid ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) → ( ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
112 111 imp ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) ⊆ ( Vtx ‘ 𝐻 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) )
113 82 112 mpd ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) )
114 113 exp31 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
115 114 com23 ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
116 70 115 sylbid ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
117 116 exp31 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) ) ) )
118 117 com23 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) ) ) )
119 118 com24 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) ) ) )
120 119 3imp ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) → ( ( 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ∧ 𝑘 = ( 𝑗 ‘ 𝑙 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
121 120 expdimp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑙 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑙 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
122 67 121 syl5d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) ∧ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
123 122 rexlimdva ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ∧ ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ) → ( ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
124 123 3exp ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) ) ) )
125 124 com25 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) ) ) )
126 125 impr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) ) )
127 126 impl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ∃ 𝑙 ∈ dom ( iEdg ‘ 𝐺 ) 𝑘 = ( 𝑗 ‘ 𝑙 ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) ) )
128 61 127 mpd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) )
129 128 rexlimdva ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ( 𝐹 “ 𝐾 ) = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) )
130 56 129 sylbid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 → ( 𝐾 ⊆ 𝑉 → 𝐾 ∈ 𝐼 ) ) )
131 130 impd ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) → 𝐾 ∈ 𝐼 ) )
132 52 131 impbid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ∧ ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )
133 132 exp31 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) ) ) )
134 133 exlimdv ⊢ ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) ) ) )
135 134 imp ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) ) )
136 7 135 syl ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( 𝐻 ∈ UHGraph ∧ 𝐺 ∈ UHGraph ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) ) )
137 136 expd ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐻 ∈ UHGraph → ( 𝐺 ∈ UHGraph → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) ) ) )
138 137 com13 ⊢ ( 𝐺 ∈ UHGraph → ( 𝐻 ∈ UHGraph → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) ) ) )
139 138 3imp ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )