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 ⊢ V = Vtx ⁡ G
ushggricedg.e ⊢ E = Edg ⁡ G
ushggricedg.s ⊢ H = V I ↾ E
Assertion ushggricedg ⊢ G ∈ USHGraph → G ≃ 𝑔𝑟 H

Proof

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