grlimprclnbgredg

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 . (Contributed by AV, 27-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	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)$

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	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\}))$
8		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), f (B)\} = g (\{A, B\}))) \to f : N \underset{1-1 onto}{⟶} M$
9		f1of	$⊢ g : K \underset{1-1 onto}{⟶} L \to g : K ⟶ L$
10	9	3ad2ant2	$⊢ (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\})) \to g : K ⟶ L$
11	10	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 g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))) \to g : K ⟶ L$
12		uspgruhgr	$⊢ G \in USHGraph \to G \in UHGraph$
13	12	adantr	$⊢ (G \in USHGraph \land H \in USHGraph) \to G \in UHGraph$
14	13	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$
15		simp33	$⊢ ((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 I$
16		prid1g	$⊢ A \in V \to A \in \{A, B\}$
17	16	3ad2ant1	$⊢ (A \in V \land B \in W \land \{A, B\} \in I) \to A \in \{A, B\}$
18	17	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\}$
19	14 15 18	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 UHGraph \land \{A, B\} \in I \land A \in \{A, B\})$
20	19	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 \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))) \to (G \in UHGraph \land \{A, B\} \in I \land A \in \{A, B\})$
21	1 2 3	clnbgrvtxedg	$⊢ (G \in UHGraph \land \{A, B\} \in I \land A \in \{A, B\}) \to \{A, B\} \in K$
22	20 21	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 g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))) \to \{A, B\} \in K$
23	11 22	ffvelcdmd	$⊢ (((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), f (B)\} = g (\{A, B\}))) \to g (\{A, B\}) \in L$
24		eleq1	$⊢ \{f (A), f (B)\} = g (\{A, B\}) \to (\{f (A), f (B)\} \in L \leftrightarrow g (\{A, B\}) \in L)$
25	24	3ad2ant3	$⊢ (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\})) \to (\{f (A), f (B)\} \in L \leftrightarrow g (\{A, B\}) \in L)$
26	25	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 g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))) \to (\{f (A), f (B)\} \in L \leftrightarrow g (\{A, B\}) \in L)$
27	23 26	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 \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))) \to \{f (A), f (B)\} \in L$
28	8 27	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 g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\}))) \to (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L)$
29	28	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), f (B)\} = g (\{A, B\})) \to (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L))$
30	29	exlimdv	$⊢ ((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 g (f : N \underset{1-1 onto}{⟶} M \land g : K \underset{1-1 onto}{⟶} L \land \{f (A), f (B)\} = g (\{A, B\})) \to (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L))$
31	30	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 \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\})) \to \exists f (f : N \underset{1-1 onto}{⟶} M \land \{f (A), f (B)\} \in L))$
32	7 31	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)$

Metamath Proof Explorer

Theorem grlimprclnbgredg

Proof