grlimedgclnbgr

Description: For two locally isomorphic graphs G and H and a vertex A of G there are two bijections f and g mapping the closed neighborhood N of A onto the closed neighborhood M of ( FA ) and the edges between the vertices in N onto the edges between the vertices in M , so that the mapped vertices of an edge E containing the vertex A is an edge between the vertices in M . (Contributed by AV, 25-Dec-2025)

	Ref	Expression
Hypotheses	clnbgrvtxedg.n	$⊢ N = G ClNeighbVtx A$
	clnbgrvtxedg.i	$⊢ I = Edg (G)$
	clnbgrvtxedg.k	$⊢ K = \{x \in I \| x \subseteq N\}$
	grlimedgclnbgr.m	$⊢ M = H ClNeighbVtx F (A)$
	grlimedgclnbgr.j	$⊢ J = Edg (H)$
	grlimedgclnbgr.l	$⊢ L = \{x \in J \| x \subseteq M\}$
Assertion	grlimedgclnbgr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E))$

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxedg.n	$⊢ N = G ClNeighbVtx A$
2		clnbgrvtxedg.i	$⊢ I = Edg (G)$
3		clnbgrvtxedg.k	$⊢ K = \{x \in I \| x \subseteq N\}$
4		grlimedgclnbgr.m	$⊢ M = H ClNeighbVtx F (A)$
5		grlimedgclnbgr.j	$⊢ J = Edg (H)$
6		grlimedgclnbgr.l	$⊢ L = \{x \in J \| x \subseteq M\}$
7		simp1l	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to G \in USHGraph$
8		simp1r	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to H \in USHGraph$
9		simp2	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to F \in (G GraphLocIso H)$
10		eqid	$⊢ Vtx (G) = Vtx (G)$
11		eqid	$⊢ Vtx (H) = Vtx (H)$
12		eqid	$⊢ G ClNeighbVtx v = G ClNeighbVtx v$
13		eqid	$⊢ H ClNeighbVtx F (v) = H ClNeighbVtx F (v)$
14		sseq1	$⊢ x = y \to (x \subseteq G ClNeighbVtx v \leftrightarrow y \subseteq G ClNeighbVtx v)$
15	14	cbvrabv	$⊢ \{x \in I \| x \subseteq G ClNeighbVtx v\} = \{y \in I \| y \subseteq G ClNeighbVtx v\}$
16		sseq1	$⊢ x = y \to (x \subseteq H ClNeighbVtx F (v) \leftrightarrow y \subseteq H ClNeighbVtx F (v))$
17	16	cbvrabv	$⊢ \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} = \{y \in J \| y \subseteq H ClNeighbVtx F (v)\}$
18	10 11 12 13 2 5 15 17	usgrlimprop	$⊢ (G \in USHGraph \land H \in USHGraph \land F \in (G GraphLocIso H)) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))))$
19	7 8 9 18	syl3anc	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to (F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))))$
20		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
21	20	adantr	$⊢ (G \in USHGraph \land H \in USHGraph) \to G \in UHGraph$
22	21	3ad2ant1	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to G \in UHGraph$
23	2	eleq2i	$⊢ E \in I \leftrightarrow E \in Edg (G)$
24	23	biimpi	$⊢ E \in I \to E \in Edg (G)$
25	24	adantr	$⊢ (E \in I \land A \in E) \to E \in Edg (G)$
26	25	3ad2ant3	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to E \in Edg (G)$
27		simp3r	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to A \in E$
28		uhgredgrnv	$⊢ (G \in UHGraph \land E \in Edg (G) \land A \in E) \to A \in Vtx (G)$
29	22 26 27 28	syl3anc	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to A \in Vtx (G)$
30		eqidd	$⊢ v = A \to f = f$
31		oveq2	$⊢ v = A \to G ClNeighbVtx v = G ClNeighbVtx A$
32		fveq2	$⊢ v = A \to F (v) = F (A)$
33	32	oveq2d	$⊢ v = A \to H ClNeighbVtx F (v) = H ClNeighbVtx F (A)$
34	30 31 33	f1oeq123d	$⊢ v = A \to (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \leftrightarrow f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A))$
35		eqidd	$⊢ v = A \to g = g$
36	31	sseq2d	$⊢ v = A \to (x \subseteq G ClNeighbVtx v \leftrightarrow x \subseteq G ClNeighbVtx A)$
37	36	rabbidv	$⊢ v = A \to \{x \in I \| x \subseteq G ClNeighbVtx v\} = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
38	33	sseq2d	$⊢ v = A \to (x \subseteq H ClNeighbVtx F (v) \leftrightarrow x \subseteq H ClNeighbVtx F (A))$
39	38	rabbidv	$⊢ v = A \to \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} = \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
40	35 37 39	f1oeq123d	$⊢ v = A \to (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \leftrightarrow g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\})$
41	37	raleqdv	$⊢ v = A \to (\forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e) \leftrightarrow \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))$
42	40 41	anbi12d	$⊢ v = A \to ((g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e)) \leftrightarrow (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)))$
43	42	exbidv	$⊢ v = A \to (\exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e)) \leftrightarrow \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)))$
44	34 43	anbi12d	$⊢ v = A \to ((f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))) \leftrightarrow (f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))))$
45	44	exbidv	$⊢ v = A \to (\exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))) \leftrightarrow \exists f (f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))))$
46	45	rspcv	$⊢ A \in Vtx (G) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))) \to \exists f (f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))))$
47	29 46	syl	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))) \to \exists f (f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))))$
48		eqid	$⊢ f = f$
49		id	$⊢ f = f \to f = f$
50	1	a1i	$⊢ f = f \to N = G ClNeighbVtx A$
51	4	a1i	$⊢ f = f \to M = H ClNeighbVtx F (A)$
52	49 50 51	f1oeq123d	$⊢ f = f \to (f : N \underset{1-1 onto}{⟶} M \leftrightarrow f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A))$
53	48 52	ax-mp	$⊢ f : N \underset{1-1 onto}{⟶} M \leftrightarrow f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)$
54	53	biimpri	$⊢ f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \to f : N \underset{1-1 onto}{⟶} M$
55	54	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \to f : N \underset{1-1 onto}{⟶} M$
56	55	adantr	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \land (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))) \to f : N \underset{1-1 onto}{⟶} M$
57		eqid	$⊢ g = g$
58		id	$⊢ g = g \to g = g$
59	1	sseq2i	$⊢ x \subseteq N \leftrightarrow x \subseteq G ClNeighbVtx A$
60	3 59	rabbieq	$⊢ K = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
61	60	a1i	$⊢ g = g \to K = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
62	4	sseq2i	$⊢ x \subseteq M \leftrightarrow x \subseteq H ClNeighbVtx F (A)$
63	6 62	rabbieq	$⊢ L = \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
64	63	a1i	$⊢ g = g \to L = \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
65	58 61 64	f1oeq123d	$⊢ g = g \to (g : K \underset{1-1 onto}{⟶} L \leftrightarrow g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\})$
66	57 65	ax-mp	$⊢ g : K \underset{1-1 onto}{⟶} L \leftrightarrow g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
67	66	biimpri	$⊢ g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \to g : K \underset{1-1 onto}{⟶} L$
68	67	adantr	$⊢ (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)) \to g : K \underset{1-1 onto}{⟶} L$
69	68	adantl	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \land (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))) \to g : K \underset{1-1 onto}{⟶} L$
70		simp3l	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to E \in I$
71		eqid	$⊢ G ClNeighbVtx A = G ClNeighbVtx A$
72		eqid	$⊢ \{x \in I \| x \subseteq G ClNeighbVtx A\} = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
73	71 2 72	clnbgrvtxedg	$⊢ (G \in UHGraph \land E \in I \land A \in E) \to E \in \{x \in I \| x \subseteq G ClNeighbVtx A\}$
74	22 70 27 73	syl3anc	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to E \in \{x \in I \| x \subseteq G ClNeighbVtx A\}$
75		imaeq2	$⊢ e = E \to f [e] = f [E]$
76		fveq2	$⊢ e = E \to g (e) = g (E)$
77	75 76	eqeq12d	$⊢ e = E \to (f [e] = g (e) \leftrightarrow f [E] = g (E))$
78	77	rspcv	$⊢ E \in \{x \in I \| x \subseteq G ClNeighbVtx A\} \to (\forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e) \to f [E] = g (E))$
79	74 78	syl	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to (\forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e) \to f [E] = g (E))$
80	79	adantld	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to ((g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)) \to f [E] = g (E))$
81	80	adantr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \to ((g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)) \to f [E] = g (E))$
82	81	imp	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \land (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))) \to f [E] = g (E)$
83	56 69 82	3jca	$⊢ ((((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \land (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))) \to (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E))$
84	83	ex	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \to ((g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)) \to (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E)))$
85	84	eximdv	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \land f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)) \to (\exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e)) \to \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E)))$
86	85	expimpd	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to ((f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))) \to \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E)))$
87	86	eximdv	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to (\exists f (f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx A\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (A)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx A\} f [e] = g (e))) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E)))$
88	47 87	syld	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to (\forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e))) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E)))$
89	88	adantld	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to ((F : Vtx (G) \underset{1-1 onto}{⟶} Vtx (H) \land \forall v \in Vtx (G) \exists f (f : G ClNeighbVtx v \underset{1-1 onto}{⟶} H ClNeighbVtx F (v) \land \exists g (g : \{x \in I \| x \subseteq G ClNeighbVtx v\} \underset{1-1 onto}{⟶} \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} \land \forall e \in \{x \in I \| x \subseteq G ClNeighbVtx v\} f [e] = g (e)))) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E)))$
90	19 89	mpd	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (E \in I \land A \in E)) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [E] = g (E))$

Metamath Proof Explorer

Theorem grlimedgclnbgr

Proof