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 𝐴 ) )