# Metamath Proof Explorer

## Theorem isomgrsym

Description: The isomorphy relation is symmetric for hypergraphs. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgrsym ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝐴 IsomGr 𝐵𝐵 IsomGr 𝐴 ) )

### Proof

Step Hyp Ref Expression
1 eqid ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐴 )
2 eqid ( Vtx ‘ 𝐵 ) = ( Vtx ‘ 𝐵 )
3 eqid ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐴 )
4 eqid ( iEdg ‘ 𝐵 ) = ( iEdg ‘ 𝐵 )
5 1 2 3 4 isomgr ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
6 vex 𝑓 ∈ V
7 6 cnvex 𝑓 ∈ V
8 7 a1i ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → 𝑓 ∈ V )
9 f1ocnv ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → 𝑓 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) )
10 9 adantr ( ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) → 𝑓 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) )
11 10 adantl ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → 𝑓 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) )
12 vex 𝑔 ∈ V
13 12 cnvex 𝑔 ∈ V
14 13 a1i ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → 𝑔 ∈ V )
15 f1ocnv ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) → 𝑔 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) )
16 15 adantr ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → 𝑔 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) )
17 16 3ad2ant2 ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → 𝑔 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) )
18 f1ocnvdm ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐴 ) )
19 18 3ad2antl2 ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐴 ) )
20 fveq2 ( 𝑖 = ( 𝑔𝑗 ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) )
21 20 imaeq2d ( 𝑖 = ( 𝑔𝑗 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) )
22 2fveq3 ( 𝑖 = ( 𝑔𝑗 ) → ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) )
23 21 22 eqeq12d ( 𝑖 = ( 𝑔𝑗 ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) ) )
24 23 adantl ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) ∧ 𝑖 = ( 𝑔𝑗 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) ) )
25 19 24 rspcdv ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) ) )
26 f1ocnvfv2 ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔 ‘ ( 𝑔𝑗 ) ) = 𝑗 )
27 26 3ad2antl2 ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔 ‘ ( 𝑔𝑗 ) ) = 𝑗 )
28 27 fveq2d ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) )
29 28 eqeq2d ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) )
30 f1of1 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → 𝑓 : ( Vtx ‘ 𝐴 ) –1-1→ ( Vtx ‘ 𝐵 ) )
31 30 3ad2ant3 ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → 𝑓 : ( Vtx ‘ 𝐴 ) –1-1→ ( Vtx ‘ 𝐵 ) )
32 31 adantr ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → 𝑓 : ( Vtx ‘ 𝐴 ) –1-1→ ( Vtx ‘ 𝐵 ) )
33 simpl1l ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → 𝐴 ∈ UHGraph )
34 1 3 uhgrss ( ( 𝐴 ∈ UHGraph ∧ ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ⊆ ( Vtx ‘ 𝐴 ) )
35 33 19 34 syl2anc ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ⊆ ( Vtx ‘ 𝐴 ) )
36 32 35 jca ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1→ ( Vtx ‘ 𝐵 ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ⊆ ( Vtx ‘ 𝐴 ) ) )
37 36 adantr ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) ∧ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1→ ( Vtx ‘ 𝐵 ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ⊆ ( Vtx ‘ 𝐴 ) ) )
38 f1imacnv ( ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1→ ( Vtx ‘ 𝐵 ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ⊆ ( Vtx ‘ 𝐴 ) ) → ( 𝑓 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) )
39 37 38 syl ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) ∧ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) → ( 𝑓 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) )
40 imaeq2 ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) → ( 𝑓 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) )
41 40 adantl ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) ∧ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) → ( 𝑓 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) )
42 39 41 eqtr3d ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) ∧ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) )
43 42 ex ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) )
44 29 43 sylbid ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ ( 𝑔𝑗 ) ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) )
45 25 44 syld ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) )
46 45 ex ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) ) )
47 46 com23 ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) ) )
48 47 3exp ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) ) ) ) )
49 48 com34 ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) ) ) ) )
50 49 impd ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) ) ) ) )
51 50 3imp1 ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) )
52 51 eqcomd ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) )
53 52 ralrimiva ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) )
54 17 53 jca ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → ( 𝑔 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) )
55 f1oeq1 ( = 𝑔 → ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ↔ 𝑔 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ) )
56 fveq1 ( = 𝑔 → ( 𝑗 ) = ( 𝑔𝑗 ) )
57 56 fveq2d ( = 𝑔 → ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) )
58 57 eqeq2d ( = 𝑔 → ( ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) )
59 58 ralbidv ( = 𝑔 → ( ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ↔ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) )
60 55 59 anbi12d ( = 𝑔 → ( ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ↔ ( 𝑔 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑔𝑗 ) ) ) ) )
61 14 54 60 spcedv ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) )
62 61 3exp ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
63 62 exlimdv ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
64 63 com23 ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
65 64 imp32 ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) )
66 11 65 jca ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → ( 𝑓 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) )
67 f1oeq1 ( 𝑒 = 𝑓 → ( 𝑒 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ↔ 𝑓 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ) )
68 imaeq1 ( 𝑒 = 𝑓 → ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) )
69 68 eqeq1d ( 𝑒 = 𝑓 → ( ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) )
70 69 ralbidv ( 𝑒 = 𝑓 → ( ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ↔ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) )
71 70 anbi2d ( 𝑒 = 𝑓 → ( ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ↔ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) )
72 71 exbidv ( 𝑒 = 𝑓 → ( ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ↔ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) )
73 67 72 anbi12d ( 𝑒 = 𝑓 → ( ( 𝑒 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ↔ ( 𝑓 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑓 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
74 8 66 73 spcedv ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) )
75 2 1 4 3 isomgr ( ( 𝐵𝑌𝐴 ∈ UHGraph ) → ( 𝐵 IsomGr 𝐴 ↔ ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
76 75 ancoms ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝐵 IsomGr 𝐴 ↔ ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
77 76 adantr ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → ( 𝐵 IsomGr 𝐴 ↔ ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐴 ) ∧ ∃ ( : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐴 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑒 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ ( 𝑗 ) ) ) ) ) )
78 74 77 mpbird ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) → 𝐵 IsomGr 𝐴 )
79 78 ex ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) → 𝐵 IsomGr 𝐴 ) )
80 79 exlimdv ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) → 𝐵 IsomGr 𝐴 ) )
81 5 80 sylbid ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝐴 IsomGr 𝐵𝐵 IsomGr 𝐴 ) )