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	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
	clnbgrvtxedg.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
	clnbgrvtxedg.k	⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
	grlimedgclnbgr.m	⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
	grlimedgclnbgr.j	⊢ 𝐽 = ( Edg ‘ 𝐻 )
	grlimedgclnbgr.l	⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion	grlimprclnbgr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		clnbgrvtxedg.n	⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
2		clnbgrvtxedg.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
3		clnbgrvtxedg.k	⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
4		grlimedgclnbgr.m	⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
5		grlimedgclnbgr.j	⊢ 𝐽 = ( Edg ‘ 𝐻 )
6		grlimedgclnbgr.l	⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
7		simp3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → { 𝐴 , 𝐵 } ∈ 𝐼 )
8		prid1g	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
9	8	3ad2ant1	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
10	7 9	jca	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → ( { 𝐴 , 𝐵 } ∈ 𝐼 ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) )
11	1 2 3 4 5 6	grlimedgclnbgr	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐼 ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
12	10 11	syl3an3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
13		simpr1	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
14		simpr2	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
15		f1ofn	⊢ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 → 𝑓 Fn 𝑁 )
16	15	adantl	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝑓 Fn 𝑁 )
17		uspgruhgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
18	17	adantr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UHGraph )
19	18	3ad2ant1	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐺 ∈ UHGraph )
20	2	eleq2i	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 ↔ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
21	20	biimpi	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 → { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
22	21	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
23	22	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
24	9	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
25		uhgredgrnv	⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
26	19 23 24 25	syl3anc	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
27	26	adantr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
28		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29	28	clnbgrvtxel	⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
30	27 29	syl	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
31	30 1	eleqtrrdi	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐴 ∈ 𝑁 )
32		prcom	⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
33	32	eleq1i	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 ↔ { 𝐵 , 𝐴 } ∈ 𝐼 )
34	33	biimpi	⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 → { 𝐵 , 𝐴 } ∈ 𝐼 )
35	34	3ad2ant3	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → { 𝐵 , 𝐴 } ∈ 𝐼 )
36	35	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → { 𝐵 , 𝐴 } ∈ 𝐼 )
37	36	adantr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → { 𝐵 , 𝐴 } ∈ 𝐼 )
38	37	olcd	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝐵 = 𝐴 ∨ { 𝐵 , 𝐴 } ∈ 𝐼 ) )
39		uspgrupgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
40	39	adantr	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UPGraph )
41	40	3ad2ant1	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐺 ∈ UPGraph )
42		prid2g	⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐴 , 𝐵 } )
43	42	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
44	43	3ad2ant3	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
45		uhgredgrnv	⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
46	19 23 44 45	syl3anc	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
47	41 26 46	3jca	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
48	47	adantr	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
49	28 2	clnbupgrel	⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) ↔ ( 𝐵 = 𝐴 ∨ { 𝐵 , 𝐴 } ∈ 𝐼 ) ) )
50	48 49	syl	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) ↔ ( 𝐵 = 𝐴 ∨ { 𝐵 , 𝐴 } ∈ 𝐼 ) ) )
51	38 50	mpbird	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
52	51 1	eleqtrrdi	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐵 ∈ 𝑁 )
53		fnimapr	⊢ ( ( 𝑓 Fn 𝑁 ∧ 𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑁 ) → ( 𝑓 “ { 𝐴 , 𝐵 } ) = { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } )
54	16 31 52 53	syl3anc	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝑓 “ { 𝐴 , 𝐵 } ) = { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } )
55	54	eqeq1d	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ↔ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
56	55	biimpd	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
57	56	a1d	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) )
58	57	ex	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) ) )
59	58	3imp2	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) )
60	13 14 59	3jca	⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
61	60	ex	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) )
62	61	2eximdv	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) )
63	12 62	mpd	⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )

Metamath Proof Explorer

Theorem grlimprclnbgr

Proof