grlimprclnbgrvtx

Description: For two locally isomorphic graphs G and H and a vertex A of G there is a bijection f mapping the closed neighborhood N of A onto the closed neighborhood M of ( FA ) , so that the mapped vertices of an edge { A , B } containing the vertex A is an edge between the vertices in M containing the vertex ( FA ) . (Contributed by AV, 28-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	grlimprclnbgrvtx	$⊢ ((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 (f : N \underset{1-1 onto}{⟶} M \land (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$

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	1 2 3 4 5 6	grlimprclnbgredg	$⊢ ((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 (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)$
8		simprl	$⊢ (((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 \{f (A), f (B)\} \in L)) \to f : N \underset{1-1 onto}{⟶} M$
9		sseq1	$⊢ x = \{f (A), f (B)\} \to (x \subseteq M \leftrightarrow \{f (A), f (B)\} \subseteq M)$
10	9 6	elrab2	$⊢ \{f (A), f (B)\} \in L \leftrightarrow (\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M)$
11	10	biimpi	$⊢ \{f (A), f (B)\} \in L \to (\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M)$
12	11	adantl	$⊢ (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L) \to (\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M)$
13	12	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 \land \{f (A), f (B)\} \in L)) \to (\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M)$
14		fvex	$⊢ f (A) \in V$
15		fvex	$⊢ f (B) \in V$
16	14 15	prss	$⊢ (f (A) \in M \land f (B) \in M) \leftrightarrow \{f (A), f (B)\} \subseteq M$
17		uspgrupgr	$⊢ H \in USHGraph \to H \in UPGraph$
18	17	adantl	$⊢ (G \in USHGraph \land H \in USHGraph) \to H \in UPGraph$
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 H \in UPGraph$
20	19	ad2antrr	$⊢ ((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \to H \in UPGraph$
21	4	eleq2i	$⊢ f (A) \in M \leftrightarrow f (A) \in (H ClNeighbVtx F (A))$
22	5	clnbupgreli	$⊢ (H \in UPGraph \land f (A) \in (H ClNeighbVtx F (A))) \to (f (A) = F (A) \lor \{f (A), F (A)\} \in J)$
23	22	ex	$⊢ H \in UPGraph \to (f (A) \in (H ClNeighbVtx F (A)) \to (f (A) = F (A) \lor \{f (A), F (A)\} \in J))$
24	21 23	biimtrid	$⊢ H \in UPGraph \to (f (A) \in M \to (f (A) = F (A) \lor \{f (A), F (A)\} \in J))$
25	4	eleq2i	$⊢ f (B) \in M \leftrightarrow f (B) \in (H ClNeighbVtx F (A))$
26	5	clnbupgreli	$⊢ (H \in UPGraph \land f (B) \in (H ClNeighbVtx F (A))) \to (f (B) = F (A) \lor \{f (B), F (A)\} \in J)$
27	26	ex	$⊢ H \in UPGraph \to (f (B) \in (H ClNeighbVtx F (A)) \to (f (B) = F (A) \lor \{f (B), F (A)\} \in J))$
28	25 27	biimtrid	$⊢ H \in UPGraph \to (f (B) \in M \to (f (B) = F (A) \lor \{f (B), F (A)\} \in J))$
29	24 28	anim12d	$⊢ H \in UPGraph \to ((f (A) \in M \land f (B) \in M) \to ((f (A) = F (A) \lor \{f (A), F (A)\} \in J) \land (f (B) = F (A) \lor \{f (B), F (A)\} \in J)))$
30	20 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 \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \to ((f (A) \in M \land f (B) \in M) \to ((f (A) = F (A) \lor \{f (A), F (A)\} \in J) \land (f (B) = F (A) \lor \{f (B), F (A)\} \in J)))$
31	30	imp	$⊢ (((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to ((f (A) = F (A) \lor \{f (A), F (A)\} \in J) \land (f (B) = F (A) \lor \{f (B), F (A)\} \in J))$
32		prcom	$⊢ \{f (A), f (B)\} = \{f (B), f (A)\}$
33		preq1	$⊢ f (B) = F (A) \to \{f (B), f (A)\} = \{F (A), f (A)\}$
34	32 33	eqtrid	$⊢ f (B) = F (A) \to \{f (A), f (B)\} = \{F (A), f (A)\}$
35	34	eleq1d	$⊢ f (B) = F (A) \to (\{f (A), f (B)\} \in L \leftrightarrow \{F (A), f (A)\} \in L)$
36	35	biimpcd	$⊢ \{f (A), f (B)\} \in L \to (f (B) = F (A) \to \{F (A), f (A)\} \in L)$
37	36	adantl	$⊢ (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L) \to (f (B) = F (A) \to \{F (A), f (A)\} \in L)$
38	37	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 \land \{f (A), f (B)\} \in L)) \to (f (B) = F (A) \to \{F (A), f (A)\} \in L)$
39	38	ad2antrr	$⊢ (((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to (f (B) = F (A) \to \{F (A), f (A)\} \in L)$
40		prcom	$⊢ \{f (B), F (A)\} = \{F (A), f (B)\}$
41	40	eleq1i	$⊢ \{f (B), F (A)\} \in J \leftrightarrow \{F (A), f (B)\} \in J$
42	41	biimpi	$⊢ \{f (B), F (A)\} \in J \to \{F (A), f (B)\} \in J$
43	42	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 \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to \{F (A), f (B)\} \in J$
44	20	ad2antrr	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to H \in UPGraph$
45		fvex	$⊢ F (A) \in V$
46	15 45	pm3.2i	$⊢ (f (B) \in V \land F (A) \in V)$
47	46	a1i	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to (f (B) \in V \land F (A) \in V)$
48		simpr	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to \{f (B), F (A)\} \in J$
49	44 47 48	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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to (H \in UPGraph \land (f (B) \in V \land F (A) \in V) \land \{f (B), F (A)\} \in J)$
50		eqid	$⊢ Vtx (H) = Vtx (H)$
51	50 5	upgrpredgv	$⊢ (H \in UPGraph \land (f (B) \in V \land F (A) \in V) \land \{f (B), F (A)\} \in J) \to (f (B) \in Vtx (H) \land F (A) \in Vtx (H))$
52		simpr	$⊢ (f (B) \in Vtx (H) \land F (A) \in Vtx (H)) \to F (A) \in Vtx (H)$
53	49 51 52	3syl	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to F (A) \in Vtx (H)$
54	50	clnbgrvtxel	$⊢ F (A) \in Vtx (H) \to F (A) \in (H ClNeighbVtx F (A))$
55	4	eleq2i	$⊢ F (A) \in M \leftrightarrow F (A) \in (H ClNeighbVtx F (A))$
56	54 55	sylibr	$⊢ F (A) \in Vtx (H) \to F (A) \in M$
57	53 56	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 \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to F (A) \in M$
58		simplrr	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to f (B) \in M$
59	57 58	prssd	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to \{F (A), f (B)\} \subseteq M$
60		sseq1	$⊢ x = \{F (A), f (B)\} \to (x \subseteq M \leftrightarrow \{F (A), f (B)\} \subseteq M)$
61	60 6	elrab2	$⊢ \{F (A), f (B)\} \in L \leftrightarrow (\{F (A), f (B)\} \in J \land \{F (A), f (B)\} \subseteq M)$
62	43 59 61	sylanbrc	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to \{F (A), f (B)\} \in L$
63	62	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)) \land (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to (\{f (B), F (A)\} \in J \to \{F (A), f (B)\} \in L)$
64	39 63	orim12d	$⊢ (((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to ((f (B) = F (A) \lor \{f (B), F (A)\} \in J) \to (\{F (A), f (A)\} \in L \lor \{F (A), f (B)\} \in L))$
65	64	imp	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land (f (B) = F (A) \lor \{f (B), F (A)\} \in J)) \to (\{F (A), f (A)\} \in L \lor \{F (A), f (B)\} \in L)$
66	65	orcomd	$⊢ ((((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \land (f (B) = F (A) \lor \{f (B), F (A)\} \in J)) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L)$
67	66	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)) \land (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to ((f (B) = F (A) \lor \{f (B), F (A)\} \in J) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$
68	67	adantld	$⊢ (((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to (((f (A) = F (A) \lor \{f (A), F (A)\} \in J) \land (f (B) = F (A) \lor \{f (B), F (A)\} \in J)) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$
69	31 68	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)) \land (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \land (f (A) \in M \land f (B) \in M)) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L)$
70	69	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)) \land (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \to ((f (A) \in M \land f (B) \in M) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$
71	16 70	biimtrrid	$⊢ ((((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 \{f (A), f (B)\} \in L)) \land \{f (A), f (B)\} \in J) \to (\{f (A), f (B)\} \subseteq M \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$
72	71	expimpd	$⊢ (((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 \{f (A), f (B)\} \in L)) \to ((\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$
73	13 72	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)) \land (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)) \to (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L)$
74	8 73	jca	$⊢ (((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 \{f (A), f (B)\} \in L)) \to (f : N \underset{1-1 onto}{⟶} M \land (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$
75	74	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 \{f (A), f (B)\} \in L) \to (f : N \underset{1-1 onto}{⟶} M \land (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L)))$
76	75	eximdv	$⊢ ((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 (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L) \to \exists f (f : N \underset{1-1 onto}{⟶} M \land (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L)))$
77	7 76	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 (f : N \underset{1-1 onto}{⟶} M \land (\{F (A), f (B)\} \in L \lor \{F (A), f (A)\} \in L))$

Metamath Proof Explorer

Theorem grlimprclnbgrvtx

Proof