Metamath Proof Explorer


Theorem ushrisomgr

Description: A simple hypergraph (with arbitrarily indexed edges) is isomorphic to a graph with the same vertices and the same edges, indexed by the edges themselves. (Contributed by AV, 11-Nov-2022)

Ref Expression
Hypotheses ushrisomgr.v 𝑉 = ( Vtx ‘ 𝐺 )
ushrisomgr.e 𝐸 = ( Edg ‘ 𝐺 )
ushrisomgr.s 𝐻 = ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩
Assertion ushrisomgr ( 𝐺 ∈ USHGraph → 𝐺 IsomGr 𝐻 )

Proof

Step Hyp Ref Expression
1 ushrisomgr.v 𝑉 = ( Vtx ‘ 𝐺 )
2 ushrisomgr.e 𝐸 = ( Edg ‘ 𝐺 )
3 ushrisomgr.s 𝐻 = ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩
4 1 fvexi 𝑉 ∈ V
5 4 a1i ( 𝐺 ∈ USHGraph → 𝑉 ∈ V )
6 5 resiexd ( 𝐺 ∈ USHGraph → ( I ↾ 𝑉 ) ∈ V )
7 f1oi ( I ↾ 𝑉 ) : 𝑉1-1-onto𝑉
8 7 a1i ( 𝐺 ∈ USHGraph → ( I ↾ 𝑉 ) : 𝑉1-1-onto𝑉 )
9 3 fveq2i ( Vtx ‘ 𝐻 ) = ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ )
10 2 fvexi 𝐸 ∈ V
11 id ( 𝐸 ∈ V → 𝐸 ∈ V )
12 11 resiexd ( 𝐸 ∈ V → ( I ↾ 𝐸 ) ∈ V )
13 10 12 ax-mp ( I ↾ 𝐸 ) ∈ V
14 4 13 pm3.2i ( 𝑉 ∈ V ∧ ( I ↾ 𝐸 ) ∈ V )
15 opvtxfv ( ( 𝑉 ∈ V ∧ ( I ↾ 𝐸 ) ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = 𝑉 )
16 14 15 mp1i ( 𝐺 ∈ USHGraph → ( Vtx ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = 𝑉 )
17 9 16 syl5eq ( 𝐺 ∈ USHGraph → ( Vtx ‘ 𝐻 ) = 𝑉 )
18 17 f1oeq3d ( 𝐺 ∈ USHGraph → ( ( I ↾ 𝑉 ) : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ ( I ↾ 𝑉 ) : 𝑉1-1-onto𝑉 ) )
19 8 18 mpbird ( 𝐺 ∈ USHGraph → ( I ↾ 𝑉 ) : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) )
20 fvexd ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) ∈ V )
21 eqid ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
22 1 21 ushgrf ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 𝑉 ∖ { ∅ } ) )
23 f1f1orn ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 𝑉 ∖ { ∅ } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ran ( iEdg ‘ 𝐺 ) )
24 22 23 syl ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ran ( iEdg ‘ 𝐺 ) )
25 3 fveq2i ( iEdg ‘ 𝐻 ) = ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ )
26 10 a1i ( 𝐺 ∈ USHGraph → 𝐸 ∈ V )
27 26 resiexd ( 𝐺 ∈ USHGraph → ( I ↾ 𝐸 ) ∈ V )
28 opiedgfv ( ( 𝑉 ∈ V ∧ ( I ↾ 𝐸 ) ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( I ↾ 𝐸 ) )
29 4 27 28 sylancr ( 𝐺 ∈ USHGraph → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( I ↾ 𝐸 ) )
30 25 29 syl5eq ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐻 ) = ( I ↾ 𝐸 ) )
31 30 dmeqd ( 𝐺 ∈ USHGraph → dom ( iEdg ‘ 𝐻 ) = dom ( I ↾ 𝐸 ) )
32 dmresi dom ( I ↾ 𝐸 ) = 𝐸
33 2 a1i ( 𝐺 ∈ USHGraph → 𝐸 = ( Edg ‘ 𝐺 ) )
34 edgval ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
35 33 34 eqtrdi ( 𝐺 ∈ USHGraph → 𝐸 = ran ( iEdg ‘ 𝐺 ) )
36 32 35 syl5eq ( 𝐺 ∈ USHGraph → dom ( I ↾ 𝐸 ) = ran ( iEdg ‘ 𝐺 ) )
37 31 36 eqtrd ( 𝐺 ∈ USHGraph → dom ( iEdg ‘ 𝐻 ) = ran ( iEdg ‘ 𝐺 ) )
38 37 f1oeq3d ( 𝐺 ∈ USHGraph → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ ran ( iEdg ‘ 𝐺 ) ) )
39 24 38 mpbird ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) )
40 ushgruhgr ( 𝐺 ∈ USHGraph → 𝐺 ∈ UHGraph )
41 1 21 uhgrss ( ( 𝐺 ∈ UHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑉 )
42 40 41 sylan ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑉 )
43 resiima ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ⊆ 𝑉 → ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
44 42 43 syl ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
45 f1f ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1→ ( 𝒫 𝑉 ∖ { ∅ } ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
46 22 45 syl ( 𝐺 ∈ USHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
47 46 ffund ( 𝐺 ∈ USHGraph → Fun ( iEdg ‘ 𝐺 ) )
48 fvelrn ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐺 ) )
49 47 48 sylan ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐺 ) )
50 2 34 eqtri 𝐸 = ran ( iEdg ‘ 𝐺 )
51 49 50 eleqtrrdi ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐸 )
52 fvresi ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ∈ 𝐸 → ( ( I ↾ 𝐸 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
53 51 52 syl ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( I ↾ 𝐸 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
54 10 a1i ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → 𝐸 ∈ V )
55 54 resiexd ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( I ↾ 𝐸 ) ∈ V )
56 4 55 28 sylancr ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩ ) = ( I ↾ 𝐸 ) )
57 25 56 eqtr2id ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( I ↾ 𝐸 ) = ( iEdg ‘ 𝐻 ) )
58 57 fveq1d ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( I ↾ 𝐸 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
59 44 53 58 3eqtr2d ( ( 𝐺 ∈ USHGraph ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
60 59 ralrimiva ( 𝐺 ∈ USHGraph → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
61 39 60 jca ( 𝐺 ∈ USHGraph → ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
62 f1oeq1 ( 𝑔 = ( iEdg ‘ 𝐺 ) → ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ↔ ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) )
63 fveq1 ( 𝑔 = ( iEdg ‘ 𝐺 ) → ( 𝑔𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
64 63 fveq2d ( 𝑔 = ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
65 64 eqeq2d ( 𝑔 = ( iEdg ‘ 𝐺 ) → ( ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ↔ ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
66 65 ralbidv ( 𝑔 = ( iEdg ‘ 𝐺 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
67 62 66 anbi12d ( 𝑔 = ( iEdg ‘ 𝐺 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
68 20 61 67 spcedv ( 𝐺 ∈ USHGraph → ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) )
69 19 68 jca ( 𝐺 ∈ USHGraph → ( ( I ↾ 𝑉 ) : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) )
70 f1oeq1 ( 𝑓 = ( I ↾ 𝑉 ) → ( 𝑓 : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ ( I ↾ 𝑉 ) : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ) )
71 imaeq1 ( 𝑓 = ( I ↾ 𝑉 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
72 71 eqeq1d ( 𝑓 = ( I ↾ 𝑉 ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ↔ ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) )
73 72 ralbidv ( 𝑓 = ( I ↾ 𝑉 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) )
74 73 anbi2d ( 𝑓 = ( I ↾ 𝑉 ) → ( ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) )
75 74 exbidv ( 𝑓 = ( I ↾ 𝑉 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) )
76 70 75 anbi12d ( 𝑓 = ( I ↾ 𝑉 ) → ( ( 𝑓 : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) ↔ ( ( I ↾ 𝑉 ) : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( I ↾ 𝑉 ) “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
77 6 69 76 spcedv ( 𝐺 ∈ USHGraph → ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) )
78 opex 𝑉 , ( I ↾ 𝐸 ) ⟩ ∈ V
79 3 78 eqeltri 𝐻 ∈ V
80 eqid ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
81 eqid ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
82 1 80 21 81 isomgr ( ( 𝐺 ∈ USHGraph ∧ 𝐻 ∈ V ) → ( 𝐺 IsomGr 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
83 79 82 mpan2 ( 𝐺 ∈ USHGraph → ( 𝐺 IsomGr 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑔𝑖 ) ) ) ) ) )
84 77 83 mpbird ( 𝐺 ∈ USHGraph → 𝐺 IsomGr 𝐻 )