Metamath Proof Explorer

Theorem uhgrimedgi

Description: An isomorphism between graphs preserves edges, i.e. if there is an edge in one graph connecting vertices then there is an edge in the other graph connecting the corresponding vertices. (Contributed by AV, 25-Oct-2025)

Ref Expression
Hypotheses uhgrimedgi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
uhgrimedgi.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
Assertion uhgrimedgi ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ∈ 𝐸 ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 )

Proof

Step Hyp Ref Expression
1 uhgrimedgi.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
2 uhgrimedgi.d ⊢ 𝐷 = ( Edg ‘ 𝐻 )
3 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
4 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 eqid ⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
7 3 4 5 6 grimprop ⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
8 1 eleq2i ⊢ ( 𝐾 ∈ 𝐸 ↔ 𝐾 ∈ ( Edg ‘ 𝐺 ) )
9 5 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
10 5 edgiedgb ⊢ ( Fun ( iEdg ‘ 𝐺 ) → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
11 9 10 syl ⊢ ( 𝐺 ∈ UHGraph → ( 𝐾 ∈ ( Edg ‘ 𝐺 ) ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
12 8 11 bitrid ⊢ ( 𝐺 ∈ UHGraph → ( 𝐾 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
13 12 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐾 ∈ 𝐸 ↔ ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
14 simplr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) )
15 2fveq3 ⊢ ( 𝑖 = 𝑘 → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) )
16 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) )
17 16 imaeq2d ⊢ ( 𝑖 = 𝑘 → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
18 15 17 eqeq12d ⊢ ( 𝑖 = 𝑘 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
19 18 rspcv ⊢ ( 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
20 14 19 syl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ) )
21 6 uhgrfun ⊢ ( 𝐻 ∈ UHGraph → Fun ( iEdg ‘ 𝐻 ) )
22 21 ad3antlr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → Fun ( iEdg ‘ 𝐻 ) )
23 f1of ⊢ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
24 23 adantl ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝑗 : dom ( iEdg ‘ 𝐺 ) ⟶ dom ( iEdg ‘ 𝐻 ) )
25 14 adantr ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) )
26 24 25 ffvelcdmd ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) )
27 6 iedgedg ⊢ ( ( Fun ( iEdg ‘ 𝐻 ) ∧ ( 𝑗 ‘ 𝑘 ) ∈ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐻 ) )
28 22 26 27 syl2an2r ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ ( Edg ‘ 𝐻 ) )
29 28 2 eleqtrrdi ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐷 )
30 eleq1 ⊢ ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) → ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐷 ) )
31 30 eqcoms ⊢ ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) ∈ 𝐷 ) )
32 29 31 syl5ibrcom ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
33 32 ex ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑘 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) ) )
34 20 33 syl5d ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) ) )
35 34 impd ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
36 35 ex ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) ) )
37 36 adantr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) ) )
38 37 3imp ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 )
39 imaeq2 ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 “ 𝐾 ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) )
40 39 eleq1d ⊢ ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐷 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
41 40 adantl ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐷 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
42 41 3ad2ant1 ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( ( 𝐹 “ 𝐾 ) ∈ 𝐷 ↔ ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∈ 𝐷 ) )
43 38 42 mpbird ⊢ ( ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 )
44 43 3exp ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) )
45 44 ex ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) ) )
46 45 rexlimdva ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ∃ 𝑘 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 = ( ( iEdg ‘ 𝐺 ) ‘ 𝑘 ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) ) )
47 13 46 sylbid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐾 ∈ 𝐸 → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) ) )
48 47 imp ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐾 ∈ 𝐸 ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) )
49 48 imp ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐾 ∈ 𝐸 ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )
50 49 exlimdv ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐾 ∈ 𝐸 ) ∧ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )
51 50 expimpd ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐾 ∈ 𝐸 ) → ( ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )
52 7 51 syl5 ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ 𝐾 ∈ 𝐸 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )
53 52 ex ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( 𝐾 ∈ 𝐸 → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) ) )
54 53 impcomd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) → ( ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ∈ 𝐸 ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 ) )
55 54 imp ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ) ∧ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ∧ 𝐾 ∈ 𝐸 ) ) → ( 𝐹 “ 𝐾 ) ∈ 𝐷 )