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	bilani	$⊢ (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)$
12	11	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)$
13		fvex	$⊢ f (A) \in V$
14		fvex	$⊢ f (B) \in V$
15	13 14	prss	$⊢ (f (A) \in M \land f (B) \in M) \leftrightarrow \{f (A), f (B)\} \subseteq M$
16		uspgrupgr	$⊢ H \in USHGraph \to H \in UPGraph$
17	16	adantl	$⊢ (G \in USHGraph \land H \in USHGraph) \to H \in UPGraph$
18	17	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$
19	18	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$
20	4	eleq2i	$⊢ f (A) \in M \leftrightarrow f (A) \in (H ClNeighbVtx F (A))$
21	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)$
22	21	ex	$⊢ H \in UPGraph \to (f (A) \in (H ClNeighbVtx F (A)) \to (f (A) = F (A) \lor \{f (A), F (A)\} \in J))$
23	20 22	biimtrid	$⊢ H \in UPGraph \to (f (A) \in M \to (f (A) = F (A) \lor \{f (A), F (A)\} \in J))$
24	4	eleq2i	$⊢ f (B) \in M \leftrightarrow f (B) \in (H ClNeighbVtx F (A))$
25	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)$
26	25	ex	$⊢ H \in UPGraph \to (f (B) \in (H ClNeighbVtx F (A)) \to (f (B) = F (A) \lor \{f (B), F (A)\} \in J))$
27	24 26	biimtrid	$⊢ H \in UPGraph \to (f (B) \in M \to (f (B) = F (A) \lor \{f (B), F (A)\} \in J))$
28	23 27	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)))$
29	19 28	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)))$
30	29	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))$
31		prcom	$⊢ \{f (A), f (B)\} = \{f (B), f (A)\}$
32		preq1	$⊢ f (B) = F (A) \to \{f (B), f (A)\} = \{F (A), f (A)\}$
33	31 32	eqtrid	$⊢ f (B) = F (A) \to \{f (A), f (B)\} = \{F (A), f (A)\}$
34	33	eleq1d	$⊢ f (B) = F (A) \to (\{f (A), f (B)\} \in L \leftrightarrow \{F (A), f (A)\} \in L)$
35	34	biimpcd	$⊢ \{f (A), f (B)\} \in L \to (f (B) = F (A) \to \{F (A), f (A)\} \in L)$
36	35	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)$
37	36	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)$
38	37	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)$
39		prcom	$⊢ \{f (B), F (A)\} = \{F (A), f (B)\}$
40	39	eleq1i	$⊢ \{f (B), F (A)\} \in J \leftrightarrow \{F (A), f (B)\} \in J$
41	40	bilani	$⊢ ((((((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$
42	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) \land (f (A) \in M \land f (B) \in M)) \land \{f (B), F (A)\} \in J) \to H \in UPGraph$
43		fvex	$⊢ F (A) \in V$
44	14 43	pm3.2i	$⊢ (f (B) \in V \land F (A) \in V)$
45	44	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)$
46		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$
47	42 45 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)) \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)$
48		eqid	$⊢ Vtx (H) = Vtx (H)$
49	48 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))$
50		simpr	$⊢ (f (B) \in Vtx (H) \land F (A) \in Vtx (H)) \to F (A) \in Vtx (H)$
51	47 49 50	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)$
52	48	clnbgrvtxel	$⊢ F (A) \in Vtx (H) \to F (A) \in (H ClNeighbVtx F (A))$
53	4	eleq2i	$⊢ F (A) \in M \leftrightarrow F (A) \in (H ClNeighbVtx F (A))$
54	52 53	sylibr	$⊢ F (A) \in Vtx (H) \to F (A) \in M$
55	51 54	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$
56		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$
57	55 56	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$
58		sseq1	$⊢ x = \{F (A), f (B)\} \to (x \subseteq M \leftrightarrow \{F (A), f (B)\} \subseteq M)$
59	58 6	elrab2	$⊢ \{F (A), f (B)\} \in L \leftrightarrow (\{F (A), f (B)\} \in J \land \{F (A), f (B)\} \subseteq M)$
60	41 57 59	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$
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)) \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)$
62	38 61	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))$
63	62	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)$
64	63	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)$
65	64	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))$
66	65	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))$
67	30 66	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)$
68	67	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))$
69	15 68	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))$
70	69	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))$
71	12 70	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)$
72	8 71	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))$
73	72	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)))$
74	73	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)))$
75	7 74	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