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	birani	$⊢ (E \in I \land A \in E) \to E \in Edg (G)$
25	24	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)$
26		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$
27		uhgredgrnv	$⊢ (G \in UHGraph \land E \in Edg (G) \land A \in E) \to A \in Vtx (G)$
28	22 25 26 27	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)$
29		eqidd	$⊢ v = A \to f = f$
30		oveq2	$⊢ v = A \to G ClNeighbVtx v = G ClNeighbVtx A$
31		fveq2	$⊢ v = A \to F (v) = F (A)$
32	31	oveq2d	$⊢ v = A \to H ClNeighbVtx F (v) = H ClNeighbVtx F (A)$
33	29 30 32	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))$
34		eqidd	$⊢ v = A \to g = g$
35	30	sseq2d	$⊢ v = A \to (x \subseteq G ClNeighbVtx v \leftrightarrow x \subseteq G ClNeighbVtx A)$
36	35	rabbidv	$⊢ v = A \to \{x \in I \| x \subseteq G ClNeighbVtx v\} = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
37	32	sseq2d	$⊢ v = A \to (x \subseteq H ClNeighbVtx F (v) \leftrightarrow x \subseteq H ClNeighbVtx F (A))$
38	37	rabbidv	$⊢ v = A \to \{x \in J \| x \subseteq H ClNeighbVtx F (v)\} = \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
39	34 36 38	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)\})$
40	36	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))$
41	39 40	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)))$
42	41	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)))$
43	33 42	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))))$
44	43	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))))$
45	44	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))))$
46	28 45	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))))$
47		eqid	$⊢ f = f$
48		id	$⊢ f = f \to f = f$
49	1	a1i	$⊢ f = f \to N = G ClNeighbVtx A$
50	4	a1i	$⊢ f = f \to M = H ClNeighbVtx F (A)$
51	48 49 50	f1oeq123d	$⊢ f = f \to (f : N \underset{1-1 onto}{⟶} M \leftrightarrow f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A))$
52	47 51	ax-mp	$⊢ f : N \underset{1-1 onto}{⟶} M \leftrightarrow f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A)$
53	52	biimpri	$⊢ f : G ClNeighbVtx A \underset{1-1 onto}{⟶} H ClNeighbVtx F (A) \to f : N \underset{1-1 onto}{⟶} M$
54	53	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$
55	54	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$
56		eqid	$⊢ g = g$
57		id	$⊢ g = g \to g = g$
58	1	sseq2i	$⊢ x \subseteq N \leftrightarrow x \subseteq G ClNeighbVtx A$
59	3 58	rabbieq	$⊢ K = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
60	59	a1i	$⊢ g = g \to K = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
61	4	sseq2i	$⊢ x \subseteq M \leftrightarrow x \subseteq H ClNeighbVtx F (A)$
62	6 61	rabbieq	$⊢ L = \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
63	62	a1i	$⊢ g = g \to L = \{x \in J \| x \subseteq H ClNeighbVtx F (A)\}$
64	57 60 63	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)\})$
65	56 64	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)\}$
66	65	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$
67	66	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$
68	67	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$
69		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$
70		eqid	$⊢ G ClNeighbVtx A = G ClNeighbVtx A$
71		eqid	$⊢ \{x \in I \| x \subseteq G ClNeighbVtx A\} = \{x \in I \| x \subseteq G ClNeighbVtx A\}$
72	70 2 71	clnbgrvtxedg	$⊢ (G \in UHGraph \land E \in I \land A \in E) \to E \in \{x \in I \| x \subseteq G ClNeighbVtx A\}$
73	22 69 26 72	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\}$
74		imaeq2	$⊢ e = E \to f [e] = f [E]$
75		fveq2	$⊢ e = E \to g (e) = g (E)$
76	74 75	eqeq12d	$⊢ e = E \to (f [e] = g (e) \leftrightarrow f [E] = g (E))$
77	76	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))$
78	73 77	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))$
79	78	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))$
80	79	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))$
81	80	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)$
82	55 68 81	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))$
83	82	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)))$
84	83	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)))$
85	84	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)))$
86	85	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)))$
87	46 86	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)))$
88	87	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)))$
89	19 88	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