Metamath Proof Explorer

Theorem clnbgrgrimlem

Description: Lemma for clnbgrgrim : For two isomorphic hypergraphs, if there is an edge connecting the image of a vertex of the first graph with a vertex of the second graph, the vertex of the second graph is the image of a neighbor of the vertex of the first graph. (Contributed by AV, 2-Jun-2025)

Ref Expression
Hypotheses clnbgrgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clnbgrgrimlem.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
clnbgrgrimlem.e ⊢ 𝐸 = ( Edg ‘ 𝐻 )
Assertion clnbgrgrimlem ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑌 ) )

Proof

Step Hyp Ref Expression
1 clnbgrgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 clnbgrgrimlem.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 clnbgrgrimlem.e ⊢ 𝐸 = ( Edg ‘ 𝐻 )
4 3 eleq2i ⊢ ( 𝐾 ∈ 𝐸 ↔ 𝐾 ∈ ( Edg ‘ 𝐻 ) )
5 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
6 5 uhgredgiedgb ⊢ ( 𝐻 ∈ UHGraph → ( 𝐾 ∈ ( Edg ‘ 𝐻 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
7 4 6 bitrid ⊢ ( 𝐻 ∈ UHGraph → ( 𝐾 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
8 7 adantl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐾 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
9 8 3ad2ant3 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → ( 𝐾 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
10 9 adantr ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐾 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
11 sseq2 ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ↔ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
12 11 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ↔ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) )
13 simp1 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
14 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → 𝑌 ∈ 𝑊 )
15 13 14 anim12i ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) )
16 f1ocnvdm ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 )
17 15 16 syl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 )
18 simpl ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → 𝑋 ∈ 𝑉 )
19 18 adantl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝑋 ∈ 𝑉 )
20 17 19 jca ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
21 20 ad2antrr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
22 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
23 22 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
24 23 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → Fun ( iEdg ‘ 𝐺 ) )
25 24 3ad2ant3 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) → Fun ( iEdg ‘ 𝐺 ) )
26 25 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → Fun ( iEdg ‘ 𝐺 ) )
27 simpl2l ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
28 f1ocnvdm ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) )
29 27 28 sylan ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) )
30 26 29 jca ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( Fun ( iEdg ‘ 𝐺 ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) )
31 22 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
32 30 31 syl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
33 32 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐺 ) )
34 sseq2 ⊢ ( 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) → ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑒 ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
35 34 adantl ⊢ ( ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) ∧ 𝑒 = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑒 ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
36 2fveq3 ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
37 fveq2 ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
38 37 imaeq2d ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
39 36 38 eqeq12d ⊢ ( 𝑖 = ( ◡ 𝑗 ‘ 𝑘 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
40 39 rspcv ⊢ ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
41 40 adantl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
42 simpr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
43 simp1 ⊢ ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) )
44 42 43 anim12i ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) )
45 44 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) )
46 f1ocnvfv2 ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑘 )
47 45 46 syl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) = 𝑘 )
48 47 fveqeq2d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
49 sseq2 ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ↔ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
50 49 adantl ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ↔ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
51 f1ofn ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 Fn 𝑉 )
52 51 ad2antrr ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → 𝐹 Fn 𝑉 )
53 simpr3l ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → 𝑋 ∈ 𝑉 )
54 simpl ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
55 14 3ad2ant3 ⊢ ( ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → 𝑌 ∈ 𝑊 )
56 54 55 anim12i ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) )
57 56 16 syl ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 )
58 52 53 57 3jca ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 ) )
59 58 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 ) )
60 fnimapr ⊢ ( ( 𝐹 Fn 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 ) → ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) } )
61 59 60 syl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) = { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) } )
62 56 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) )
63 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
64 62 63 syl ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
65 64 preq2d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) } = { ( 𝐹 ‘ 𝑋 ) , 𝑌 } )
66 61 65 eqtr2d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → { ( 𝐹 ‘ 𝑋 ) , 𝑌 } = ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) )
67 66 sseq1d ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ↔ ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
68 f1of1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 –1-1→ 𝑊 )
69 68 adantr ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
70 69 ad2antrr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → 𝐹 : 𝑉 –1-1→ 𝑊 )
71 53 57 prssd ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑉 )
72 71 adantr ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑉 )
73 simpr2l ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → 𝐺 ∈ UHGraph )
74 1 22 uhgrss ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ⊆ 𝑉 )
75 73 74 sylan ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ⊆ 𝑉 )
76 f1imass ⊢ ( ( 𝐹 : 𝑉 –1-1→ 𝑊 ∧ ( { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑉 ∧ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ⊆ 𝑉 ) ) → ( ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
77 70 72 75 76 syl12anc ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ↔ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
78 77 biimpd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( 𝐹 “ { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ) ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
79 67 78 sylbid ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
80 79 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
81 50 80 sylbid ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
82 81 ex ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
83 48 82 sylbid ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
84 41 83 syld ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) ∧ ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
85 84 ex ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ) )
86 85 com23 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) ∧ ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ) )
87 86 3exp2 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ) ) ) ) )
88 87 com25 ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ) ) ) ) )
89 88 expimpd ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ) ) ) ) )
90 89 3imp1 ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) ) )
91 90 imp ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( ◡ 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐺 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) ) )
92 29 91 mpd ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) ) )
93 92 imp ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ ( ( iEdg ‘ 𝐺 ) ‘ ( ◡ 𝑗 ‘ 𝑘 ) ) )
94 33 35 93 rspcedvd ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑒 )
95 94 olcd ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( ( ◡ 𝐹 ‘ 𝑌 ) = 𝑋 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑒 ) )
96 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
97 1 96 clnbgrel ⊢ ( ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ↔ ( ( ( ◡ 𝐹 ‘ 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( ( ◡ 𝐹 ‘ 𝑌 ) = 𝑋 ∨ ∃ 𝑒 ∈ ( Edg ‘ 𝐺 ) { 𝑋 , ( ◡ 𝐹 ‘ 𝑌 ) } ⊆ 𝑒 ) ) )
98 21 95 97 sylanbrc ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
99 98 ex ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) )
100 99 adantr ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) )
101 12 100 sylbid ⊢ ( ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) )
102 101 ex ⊢ ( ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) ) → ( 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) )
103 102 rexlimdva ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐻 ) 𝐾 = ( ( iEdg ‘ 𝐻 ) ‘ 𝑘 ) → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) )
104 10 103 sylbid ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐾 ∈ 𝐸 → ( { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) )
105 104 impd ⊢ ( ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ∧ ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) )
106 105 3exp1 ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) ) ) )
107 106 exlimdv ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) ) ) )
108 107 imp ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) ) )
109 1 2 22 5 grimprop ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
110 108 109 syl11 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ) ) ) )
111 110 3imp1 ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) ) → ( ◡ 𝐹 ‘ 𝑌 ) ∈ ( 𝐺 ClNeighbVtx 𝑋 ) )
112 fveqeq2 ⊢ ( 𝑛 = ( ◡ 𝐹 ‘ 𝑌 ) → ( ( 𝐹 ‘ 𝑛 ) = 𝑌 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 ) )
113 112 adantl ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) ) ∧ 𝑛 = ( ◡ 𝐹 ‘ 𝑌 ) ) → ( ( 𝐹 ‘ 𝑛 ) = 𝑌 ↔ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 ) )
114 1 2 grimf1o ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
115 114 14 anim12i ⊢ ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) )
116 115 3adant1 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) )
117 116 adantr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑌 ∈ 𝑊 ) )
118 117 63 syl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑌 ) ) = 𝑌 )
119 111 113 118 rspcedvd ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) ∧ ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑌 )
120 119 ex ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) ) → ( ( 𝐾 ∈ 𝐸 ∧ { ( 𝐹 ‘ 𝑋 ) , 𝑌 } ⊆ 𝐾 ) → ∃ 𝑛 ∈ ( 𝐺 ClNeighbVtx 𝑋 ) ( 𝐹 ‘ 𝑛 ) = 𝑌 ) )