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

Proof

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