grlimprclnbgr

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 { A , B } 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	grlimprclnbgr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))$

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		simp3	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to \{A, B\} \in I$
8		prid1g	$⊢ A \in V \to A \in \{A, B\}$
9	8	3ad2ant1	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to A \in \{A, B\}$
10	7 9	jca	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to (\{A, B\} \in I \land A \in \{A, B\})$
11	1 2 3 4 5 6	grlimedgclnbgr	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (\{A, B\} \in I \land A \in \{A, B\})) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\}))$
12	10 11	syl3an3	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\}))$
13		simpr1	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\}))) \to f : N \underset{1-1 onto}{⟶} M$
14		simpr2	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\}))) \to g : K \underset{1-1 onto}{⟶} L$
15		f1ofn	$⊢ f : N \underset{1-1 onto}{⟶} M \to f Fn N$
16	15	adantl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to f Fn N$
17		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
18	17	adantr	$⊢ (G \in USHGraph \land H \in USHGraph) \to G \in UHGraph$
19	18	3ad2ant1	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to G \in UHGraph$
20	2	eleq2i	$⊢ \{A, B\} \in I \leftrightarrow \{A, B\} \in Edg (G)$
21	20	biimpi	$⊢ \{A, B\} \in I \to \{A, B\} \in Edg (G)$
22	21	3ad2ant3	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to \{A, B\} \in Edg (G)$
23	22	3ad2ant3	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to \{A, B\} \in Edg (G)$
24	9	3ad2ant3	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to A \in \{A, B\}$
25		uhgredgrnv	$⊢ (G \in UHGraph \land \{A, B\} \in Edg (G) \land A \in \{A, B\}) \to A \in Vtx (G)$
26	19 23 24 25	syl3anc	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to A \in Vtx (G)$
27	26	adantr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to A \in Vtx (G)$
28		eqid	$⊢ Vtx (G) = Vtx (G)$
29	28	clnbgrvtxel	$⊢ A \in Vtx (G) \to A \in (G ClNeighbVtx A)$
30	27 29	syl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to A \in (G ClNeighbVtx A)$
31	30 1	eleqtrrdi	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to A \in N$
32		prcom	$⊢ \{A, B\} = \{B, A\}$
33	32	eleq1i	$⊢ \{A, B\} \in I \leftrightarrow \{B, A\} \in I$
34	33	biimpi	$⊢ \{A, B\} \in I \to \{B, A\} \in I$
35	34	3ad2ant3	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to \{B, A\} \in I$
36	35	3ad2ant3	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to \{B, A\} \in I$
37	36	adantr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to \{B, A\} \in I$
38	37	olcd	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to (B = A \lor \{B, A\} \in I)$
39		uspgrupgr	$⊢ G \in USHGraph \to G \in UPGraph$
40	39	adantr	$⊢ (G \in USHGraph \land H \in USHGraph) \to G \in UPGraph$
41	40	3ad2ant1	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to G \in UPGraph$
42		prid2g	$⊢ B \in W \to B \in \{A, B\}$
43	42	3ad2ant2	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to B \in \{A, B\}$
44	43	3ad2ant3	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to B \in \{A, B\}$
45		uhgredgrnv	$⊢ (G \in UHGraph \land \{A, B\} \in Edg (G) \land B \in \{A, B\}) \to B \in Vtx (G)$
46	19 23 44 45	syl3anc	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to B \in Vtx (G)$
47	41 26 46	3jca	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to (G \in UPGraph \land A \in Vtx (G) \land B \in Vtx (G))$
48	47	adantr	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to (G \in UPGraph \land A \in Vtx (G) \land B \in Vtx (G))$
49	28 2	clnbupgrel	$⊢ (G \in UPGraph \land A \in Vtx (G) \land B \in Vtx (G)) \to (B \in (G ClNeighbVtx A) \leftrightarrow (B = A \lor \{B, A\} \in I))$
50	48 49	syl	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to (B \in (G ClNeighbVtx A) \leftrightarrow (B = A \lor \{B, A\} \in I))$
51	38 50	mpbird	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to B \in (G ClNeighbVtx A)$
52	51 1	eleqtrrdi	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to B \in N$
53		fnimapr	$⊢ (f Fn N \land A \in N \land B \in N) \to f [\{A, B\}] = \{f (A), f (B)\}$
54	16 31 52 53	syl3anc	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to f [\{A, B\}] = \{f (A), f (B)\}$
55	54	eqeq1d	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to (f [\{A, B\}] = g (\{A, B\}) \leftrightarrow \{f (A), f (B)\} = g (\{A, B\}))$
56	55	biimpd	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to (f [\{A, B\}] = g (\{A, B\}) \to \{f (A), f (B)\} = g (\{A, B\}))$
57	56	a1d	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land f : N \underset{1-1 onto}{⟶} M) \to (g : K \underset{1-1 onto}{⟶} L \to (f [\{A, B\}] = g (\{A, B\}) \to \{f (A), f (B)\} = g (\{A, B\})))$
58	57	ex	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to (f : N \underset{1-1 onto}{⟶} M \to (g : K \underset{1-1 onto}{⟶} L \to (f [\{A, B\}] = g (\{A, B\}) \to \{f (A), f (B)\} = g (\{A, B\}))))$
59	58	3imp2	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\}))) \to \{f (A), f (B)\} = g (\{A, B\})$
60	13 14 59	3jca	$⊢ (((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \land (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\}))) \to (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))$
61	60	ex	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to ((f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\})) \to (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\})))$
62	61	2eximdv	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to (\exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land f [\{A, B\}] = g (\{A, B\})) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\})))$
63	12 62	mpd	$⊢ ((G \in USHGraph \land H \in USHGraph) \land F \in (G GraphLocIso H) \land (A \in V \land B \in W \land \{A, B\} \in I)) \to \exists f \exists g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))$

Metamath Proof Explorer

Theorem grlimprclnbgr

Proof