Metamath Proof Explorer

Theorem isomgreqve

Description: A set is isomorphic to a hypergraph if it has the same vertices and the same edges. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgreqve ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → 𝐴 IsomGr 𝐵 )

Proof

Step Hyp Ref Expression
1 fvexd ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( Vtx ‘ 𝐵 ) ∈ V )
2 1 resiexd ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ ( Vtx ‘ 𝐵 ) ) ∈ V )
3 f1oi ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐵 )
4 simprl ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) )
5 4 f1oeq2d ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ↔ ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) )
6 3 5 mpbiri ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) )
7 fvexd ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( iEdg ‘ 𝐵 ) ∈ V )
8 7 dmexd ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → dom ( iEdg ‘ 𝐵 ) ∈ V )
9 8 resiexd ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ∈ V )
10 f1oi ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 )
11 simprr ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) )
12 11 dmeqd ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → dom ( iEdg ‘ 𝐴 ) = dom ( iEdg ‘ 𝐵 ) )
13 12 f1oeq2d ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ↔ ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ) )
14 10 13 mpbiri ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) )
15 eqid ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐴 )
16 eqid ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐴 )
17 15 16 uhgrss ( ( 𝐴 ∈ UHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) )
18 17 ad4ant14 ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) )
19 sseq2 ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
20 19 adantr ( ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
21 20 adantl ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
22 21 adantr ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐴 ) ↔ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) ) )
23 18 22 mpbid ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) )
24 resiima ( ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ⊆ ( Vtx ‘ 𝐵 ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) )
25 23 24 syl ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) )
26 fvresi ( 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) → ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = 𝑖 )
27 26 adantl ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = 𝑖 )
28 27 fveq2d ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) )
29 id ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) )
30 dmeq ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → dom ( iEdg ‘ 𝐴 ) = dom ( iEdg ‘ 𝐵 ) )
31 30 reseq2d ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( I ↾ dom ( iEdg ‘ 𝐴 ) ) = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) )
32 31 fveq1d ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) )
33 29 32 fveq12d ( ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
34 33 adantl ( ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
35 34 adantl ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
36 35 adantr ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
37 25 28 36 3eqtr2d ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
38 37 ralrimiva ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
39 14 38 jca ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) )
40 f1oeq1 ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ↔ ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ) )
41 fveq1 ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑔𝑖 ) = ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) )
42 41 fveq2d ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) )
43 42 eqeq2d ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) )
44 43 ralbidv ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) )
45 40 44 anbi12d ( 𝑔 = ( I ↾ dom ( iEdg ‘ 𝐵 ) ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( I ↾ dom ( iEdg ‘ 𝐵 ) ) ‘ 𝑖 ) ) ) ) )
46 9 39 45 spcedv ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) )
47 6 46 jca ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) )
48 f1oeq1 ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ↔ ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) )
49 imaeq1 ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) )
50 49 eqeq1d ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) )
51 50 ralbidv ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) )
52 51 anbi2d ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) )
53 52 exbidv ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) )
54 48 53 anbi12d ( 𝑓 = ( I ↾ ( Vtx ‘ 𝐵 ) ) → ( ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ↔ ( ( I ↾ ( Vtx ‘ 𝐵 ) ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( ( I ↾ ( Vtx ‘ 𝐵 ) ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
55 2 47 54 spcedv ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) )
56 eqid ( Vtx ‘ 𝐵 ) = ( Vtx ‘ 𝐵 )
57 eqid ( iEdg ‘ 𝐵 ) = ( iEdg ‘ 𝐵 )
58 15 56 16 57 isomgr ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
59 58 adantr ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
60 55 59 mpbird ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵𝑌 ) ∧ ( ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐵 ) ) ) → 𝐴 IsomGr 𝐵 )