grlimpredg

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 in H . (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	grlimpredg	$⊢ ((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 J)$

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		sseq1	$⊢ x = \{f (A), f (B)\} \to (x \subseteq M \leftrightarrow \{f (A), f (B)\} \subseteq M)$
9	8 6	elrab2	$⊢ \{f (A), f (B)\} \in L \leftrightarrow (\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M)$
10		simpl	$⊢ (\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M) \to \{f (A), f (B)\} \in J$
11	10	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) \to ((\{f (A), f (B)\} \in J \land \{f (A), f (B)\} \subseteq M) \to \{f (A), f (B)\} \in J)$
12	9 11	biimtrid	$⊢ (((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), f (B)\} \in L \to \{f (A), f (B)\} \in J)$
13	12	imdistanda	$⊢ ((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 J))$
14	13	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 J))$
15	7 14	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 J)$

Metamath Proof Explorer

Theorem grlimpredg

Proof