Metamath Proof Explorer

Theorem ushggricedg

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 ushggricedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
ushggricedg.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
ushggricedg.s ⊢ 𝐻 = ⟨ 𝑉 , ( I ↾ 𝐸 ) ⟩
Assertion ushggricedg ( 𝐺 ∈ USHGraph → 𝐺 ≃𝑔𝑟 𝐻 )

Proof

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