Metamath Proof Explorer

Theorem isomgreqve

Description: A set is isomorphic to a hypergraph if it has the same vertices and the same edges. (Contributed by AV, 11-Nov-2022)

Ref Expression
Assertion isomgreqve ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → A IsomGr B

Proof

Step Hyp Ref Expression
1 fvexd ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → Vtx ⁡ B ∈ V
2 1 resiexd ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ Vtx ⁡ B ∈ V
3 f1oi ⊢ I ↾ Vtx ⁡ B : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ B
4 simprl ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → Vtx ⁡ A = Vtx ⁡ B
5 4 f1oeq2d ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ Vtx ⁡ B : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ↔ I ↾ Vtx ⁡ B : Vtx ⁡ B ⟶ 1-1 onto Vtx ⁡ B
6 3 5 mpbiri ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ Vtx ⁡ B : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B
7 fvexd ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ B ∈ V
8 7 dmexd ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → dom ⁡ iEdg ⁡ B ∈ V
9 8 resiexd ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ dom ⁡ iEdg ⁡ B ∈ V
10 f1oi ⊢ I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
11 simprr ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A = iEdg ⁡ B
12 11 dmeqd ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → dom ⁡ iEdg ⁡ A = dom ⁡ iEdg ⁡ B
13 12 f1oeq2d ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ↔ I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
14 10 13 mpbiri ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
15 eqid ⊢ Vtx ⁡ A = Vtx ⁡ A
16 eqid ⊢ iEdg ⁡ A = iEdg ⁡ A
17 15 16 uhgrss ⊢ A ∈ UHGraph ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ A
18 17 ad4ant14 ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ A
19 sseq2 ⊢ Vtx ⁡ A = Vtx ⁡ B → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ A ↔ iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ B
20 19 adantr ⊢ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ A ↔ iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ B
21 20 adantl ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ A ↔ iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ B
22 21 adantr ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ A ↔ iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ B
23 18 22 mpbid ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ B
24 resiima ⊢ iEdg ⁡ A ⁡ i ⊆ Vtx ⁡ B → I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ A ⁡ i
25 23 24 syl ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ A ⁡ i
26 fvresi ⊢ i ∈ dom ⁡ iEdg ⁡ A → I ↾ dom ⁡ iEdg ⁡ A ⁡ i = i
27 26 adantl ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → I ↾ dom ⁡ iEdg ⁡ A ⁡ i = i
28 27 fveq2d ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ I ↾ dom ⁡ iEdg ⁡ A ⁡ i = iEdg ⁡ A ⁡ i
29 id ⊢ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A = iEdg ⁡ B
30 dmeq ⊢ iEdg ⁡ A = iEdg ⁡ B → dom ⁡ iEdg ⁡ A = dom ⁡ iEdg ⁡ B
31 30 reseq2d ⊢ iEdg ⁡ A = iEdg ⁡ B → I ↾ dom ⁡ iEdg ⁡ A = I ↾ dom ⁡ iEdg ⁡ B
32 31 fveq1d ⊢ iEdg ⁡ A = iEdg ⁡ B → I ↾ dom ⁡ iEdg ⁡ A ⁡ i = I ↾ dom ⁡ iEdg ⁡ B ⁡ i
33 29 32 fveq12d ⊢ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A ⁡ I ↾ dom ⁡ iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
34 33 adantl ⊢ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A ⁡ I ↾ dom ⁡ iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
35 34 adantl ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → iEdg ⁡ A ⁡ I ↾ dom ⁡ iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
36 35 adantr ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ I ↾ dom ⁡ iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
37 25 28 36 3eqtr2d ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B ∧ i ∈ dom ⁡ iEdg ⁡ A → I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
38 37 ralrimiva ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
39 14 38 jca ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
40 f1oeq1 ⊢ g = I ↾ dom ⁡ iEdg ⁡ B → g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ↔ I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
41 fveq1 ⊢ g = I ↾ dom ⁡ iEdg ⁡ B → g ⁡ i = I ↾ dom ⁡ iEdg ⁡ B ⁡ i
42 41 fveq2d ⊢ g = I ↾ dom ⁡ iEdg ⁡ B → iEdg ⁡ B ⁡ g ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
43 42 eqeq2d ⊢ g = I ↾ dom ⁡ iEdg ⁡ B → I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
44 43 ralbidv ⊢ g = I ↾ dom ⁡ iEdg ⁡ B → ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
45 40 44 anbi12d ⊢ g = I ↾ dom ⁡ iEdg ⁡ B → g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ I ↾ dom ⁡ iEdg ⁡ B : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ I ↾ dom ⁡ iEdg ⁡ B ⁡ i
46 9 39 45 spcedv ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
47 6 46 jca ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → I ↾ Vtx ⁡ B : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
48 f1oeq1 ⊢ f = I ↾ Vtx ⁡ B → f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ↔ I ↾ Vtx ⁡ B : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B
49 imaeq1 ⊢ f = I ↾ Vtx ⁡ B → f iEdg ⁡ A ⁡ i = I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i
50 49 eqeq1d ⊢ f = I ↾ Vtx ⁡ B → f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
51 50 ralbidv ⊢ f = I ↾ Vtx ⁡ B → ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
52 51 anbi2d ⊢ f = I ↾ Vtx ⁡ B → g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
53 52 exbidv ⊢ f = I ↾ Vtx ⁡ B → ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
54 48 53 anbi12d ⊢ f = I ↾ Vtx ⁡ B → f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i ↔ I ↾ Vtx ⁡ B : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A I ↾ Vtx ⁡ B iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
55 2 47 54 spcedv ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → ∃ f f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
56 eqid ⊢ Vtx ⁡ B = Vtx ⁡ B
57 eqid ⊢ iEdg ⁡ B = iEdg ⁡ B
58 15 56 16 57 isomgr ⊢ A ∈ UHGraph ∧ B ∈ Y → A IsomGr B ↔ ∃ f f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
59 58 adantr ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → A IsomGr B ↔ ∃ f f : Vtx ⁡ A ⟶ 1-1 onto Vtx ⁡ B ∧ ∃ g g : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ g ⁡ i
60 55 59 mpbird ⊢ A ∈ UHGraph ∧ B ∈ Y ∧ Vtx ⁡ A = Vtx ⁡ B ∧ iEdg ⁡ A = iEdg ⁡ B → A IsomGr B