Metamath Proof Explorer

Theorem uspgrlim

Description: A local isomorphism of simple pseudographs is a bijection between their vertices that preserves neighborhoods, expressed by properties of their edges (not edge functions as in isgrlim2 ). (Contributed by AV, 15-Aug-2025)

Ref Expression
Hypotheses uspgrlim.v ⊢ V = Vtx ⁡ G
uspgrlim.w ⊢ W = Vtx ⁡ H
uspgrlim.n ⊢ N = G ClNeighbVtx v
uspgrlim.m ⊢ M = H ClNeighbVtx F ⁡ v
uspgrlim.i ⊢ I = Edg ⁡ G
uspgrlim.j ⊢ J = Edg ⁡ H
uspgrlim.k ⊢ K = x ∈ I | x ⊆ N
uspgrlim.l ⊢ L = x ∈ J | x ⊆ M
Assertion uspgrlim ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e

Proof

Step Hyp Ref Expression
1 uspgrlim.v ⊢ V = Vtx ⁡ G
2 uspgrlim.w ⊢ W = Vtx ⁡ H
3 uspgrlim.n ⊢ N = G ClNeighbVtx v
4 uspgrlim.m ⊢ M = H ClNeighbVtx F ⁡ v
5 uspgrlim.i ⊢ I = Edg ⁡ G
6 uspgrlim.j ⊢ J = Edg ⁡ H
7 uspgrlim.k ⊢ K = x ∈ I | x ⊆ N
8 uspgrlim.l ⊢ L = x ∈ J | x ⊆ M
9 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
10 eqid ⊢ iEdg ⁡ H = iEdg ⁡ H
11 eqid ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N
12 eqid ⊢ x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M = x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
13 1 2 3 4 9 10 11 12 isgrlim2 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i
14 fvex ⊢ iEdg ⁡ H ∈ V
15 vex ⊢ h ∈ V
16 14 15 coex ⊢ iEdg ⁡ H ∘ h ∈ V
17 fvex ⊢ iEdg ⁡ G ∈ V
18 17 cnvex ⊢ iEdg ⁡ G -1 ∈ V
19 16 18 coex ⊢ iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ∈ V
20 19 a1i ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ∈ V
21 9 uspgrf1oedg ⊢ G ∈ USHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G
22 21 ad2antrr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G
23 simprl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
24 10 uspgrf1oedg ⊢ H ∈ USHGraph → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H
25 24 ad2antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H
26 ssrab2 ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⊆ dom ⁡ iEdg ⁡ G
27 ssrab2 ⊢ x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ⊆ dom ⁡ iEdg ⁡ H
28 26 27 pm3.2i ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⊆ dom ⁡ iEdg ⁡ G ∧ x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ⊆ dom ⁡ iEdg ⁡ H
29 28 a1i ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⊆ dom ⁡ iEdg ⁡ G ∧ x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ⊆ dom ⁡ iEdg ⁡ H
30 3f1oss1 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H ∧ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⊆ dom ⁡ iEdg ⁡ G ∧ x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ⊆ dom ⁡ iEdg ⁡ H → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : iEdg ⁡ G x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto iEdg ⁡ H x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
31 22 23 25 29 30 syl31anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : iEdg ⁡ G x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto iEdg ⁡ H x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
32 eqidd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1
33 3 5 7 uspgrlimlem1 ⊢ G ∈ USHGraph → K = iEdg ⁡ G x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N
34 33 ad2antrr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → K = iEdg ⁡ G x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N
35 4 6 8 uspgrlimlem1 ⊢ H ∈ USHGraph → L = iEdg ⁡ H x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
36 35 ad2antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → L = iEdg ⁡ H x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
37 32 34 36 f1oeq123d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : K ⟶ 1-1 onto L ↔ iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : iEdg ⁡ G x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto iEdg ⁡ H x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
38 31 37 mpbird ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : K ⟶ 1-1 onto L
39 simpll ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → G ∈ USHGraph
40 simprr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i
41 1 2 3 4 5 6 7 8 uspgrlimlem3 ⊢ G ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ K → f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
42 39 23 40 41 syl3anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → e ∈ K → f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
43 42 ralrimiv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → ∀ e ∈ K f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
44 38 43 jca ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
45 f1oeq1 ⊢ g = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 → g : K ⟶ 1-1 onto L ↔ iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : K ⟶ 1-1 onto L
46 fveq1 ⊢ g = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 → g ⁡ e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
47 46 eqeq2d ⊢ g = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 → f e = g ⁡ e ↔ f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
48 47 ralbidv ⊢ g = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 → ∀ e ∈ K f e = g ⁡ e ↔ ∀ e ∈ K f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
49 45 48 anbi12d ⊢ g = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 → g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e ↔ iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = iEdg ⁡ H ∘ h ∘ iEdg ⁡ G -1 ⁡ e
50 20 44 49 spcedv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
51 50 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
52 51 exlimdv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i → ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
53 14 cnvex ⊢ iEdg ⁡ H -1 ∈ V
54 vex ⊢ g ∈ V
55 53 54 coex ⊢ iEdg ⁡ H -1 ∘ g ∈ V
56 55 17 coex ⊢ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ∈ V
57 56 a1i ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ∈ V
58 21 ad2antrr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G
59 simprl ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → g : K ⟶ 1-1 onto L
60 24 ad2antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H
61 5 rabeqi ⊢ x ∈ I | x ⊆ N = x ∈ Edg ⁡ G | x ⊆ N
62 7 61 eqtri ⊢ K = x ∈ Edg ⁡ G | x ⊆ N
63 62 ssrab3 ⊢ K ⊆ Edg ⁡ G
64 6 rabeqi ⊢ x ∈ J | x ⊆ M = x ∈ Edg ⁡ H | x ⊆ M
65 8 64 eqtri ⊢ L = x ∈ Edg ⁡ H | x ⊆ M
66 65 ssrab3 ⊢ L ⊆ Edg ⁡ H
67 63 66 pm3.2i ⊢ K ⊆ Edg ⁡ G ∧ L ⊆ Edg ⁡ H
68 67 a1i ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → K ⊆ Edg ⁡ G ∧ L ⊆ Edg ⁡ H
69 3f1oss2 ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 1-1 onto Edg ⁡ G ∧ g : K ⟶ 1-1 onto L ∧ iEdg ⁡ H : dom ⁡ iEdg ⁡ H ⟶ 1-1 onto Edg ⁡ H ∧ K ⊆ Edg ⁡ G ∧ L ⊆ Edg ⁡ H → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : iEdg ⁡ G -1 K ⟶ 1-1 onto iEdg ⁡ H -1 L
70 58 59 60 68 69 syl31anc ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : iEdg ⁡ G -1 K ⟶ 1-1 onto iEdg ⁡ H -1 L
71 eqidd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G
72 3 5 7 uspgrlimlem2 ⊢ G ∈ USHGraph → iEdg ⁡ G -1 K = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N
73 72 ad2antrr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ G -1 K = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N
74 4 6 8 uspgrlimlem2 ⊢ H ∈ USHGraph → iEdg ⁡ H -1 L = x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
75 74 ad2antlr ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 L = x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
76 71 73 75 f1oeq123d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : iEdg ⁡ G -1 K ⟶ 1-1 onto iEdg ⁡ H -1 L ↔ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
77 70 76 mpbid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
78 fveq2 ⊢ x = i → iEdg ⁡ G ⁡ x = iEdg ⁡ G ⁡ i
79 78 sseq1d ⊢ x = i → iEdg ⁡ G ⁡ x ⊆ N ↔ iEdg ⁡ G ⁡ i ⊆ N
80 79 elrab ⊢ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ↔ i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N
81 1 2 3 4 5 6 7 8 uspgrlimlem4 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → i ∈ dom ⁡ iEdg ⁡ G ∧ iEdg ⁡ G ⁡ i ⊆ N → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
82 80 81 biimtrid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
83 82 ralrimiv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
84 77 83 jca ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
85 f1oeq1 ⊢ h = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ↔ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M
86 fveq1 ⊢ h = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G → h ⁡ i = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
87 86 fveq2d ⊢ h = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G → iEdg ⁡ H ⁡ h ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
88 87 eqeq2d ⊢ h = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G → f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
89 88 ralbidv ⊢ h = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G → ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
90 85 89 anbi12d ⊢ h = iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G → h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ iEdg ⁡ H -1 ∘ g ∘ iEdg ⁡ G ⁡ i
91 57 84 90 spcedv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i
92 91 ex ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i
93 92 exlimdv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e → ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i
94 52 93 impbid ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
95 94 anbi2d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → f : N ⟶ 1-1 onto M ∧ ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
96 95 exbidv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∃ f f : N ⟶ 1-1 onto M ∧ ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
97 96 ralbidv ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
98 97 anbi2d ⊢ G ∈ USHGraph ∧ H ∈ USHGraph → F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
99 98 3adant3 ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F ∈ Z → F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ h h : x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N ⟶ 1-1 onto x ∈ dom ⁡ iEdg ⁡ H | iEdg ⁡ H ⁡ x ⊆ M ∧ ∀ i ∈ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ N f iEdg ⁡ G ⁡ i = iEdg ⁡ H ⁡ h ⁡ i ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e
100 13 99 bitrd ⊢ G ∈ USHGraph ∧ H ∈ USHGraph ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ f f : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ e ∈ K f e = g ⁡ e