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 syl5req ⊢ ( ( 𝐺 ∈ 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 𝐻 )