Metamath Proof Explorer

Theorem isgrlim

Description: A local isomorphism of graphs is a bijection between their vertices that preserves neighborhoods. (Contributed by AV, 20-May-2025)

Ref Expression
Hypotheses isgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion isgrlim ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 df-grlim ⊢ GraphLocIso = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )
4 elex ⊢ ( 𝐺 ∈ 𝑋 → 𝐺 ∈ V )
5 4 3ad2ant1 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → 𝐺 ∈ V )
6 elex ⊢ ( 𝐻 ∈ 𝑌 → 𝐻 ∈ V )
7 6 3ad2ant2 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → 𝐻 ∈ V )
8 f1of ⊢ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑓 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
9 8 adantr ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) → 𝑓 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
10 9 adantl ⊢ ( ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) → 𝑓 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
11 fvexd ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( Vtx ‘ 𝐺 ) ∈ V )
12 fvexd ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( Vtx ‘ 𝐻 ) ∈ V )
13 10 11 12 fabexd ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ∈ V )
14 eqidd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → 𝑓 = 𝑓 )
15 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
16 15 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
17 fveq2 ⊢ ( ℎ = 𝐻 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐻 ) )
18 17 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐻 ) )
19 14 16 18 f1oeq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ↔ 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) )
20 id ⊢ ( 𝑔 = 𝐺 → 𝑔 = 𝐺 )
21 oveq1 ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx 𝑣 ) )
22 20 21 oveq12d ⊢ ( 𝑔 = 𝐺 → ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) = ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) )
23 id ⊢ ( ℎ = 𝐻 → ℎ = 𝐻 )
24 oveq1 ⊢ ( ℎ = 𝐻 → ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) )
25 23 24 oveq12d ⊢ ( ℎ = 𝐻 → ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) = ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) )
26 22 25 breqan12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) )
27 16 26 raleqbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) )
28 19 27 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ↔ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ) )
29 28 abbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } = { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )
30 3 5 7 13 29 elovmpod ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ) )
31 f1oeq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) )
32 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑣 ) )
33 32 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) )
34 33 oveq2d ⊢ ( 𝑓 = 𝐹 → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) = ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) )
35 34 breq2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) )
36 35 ralbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) )
37 31 36 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) ↔ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
38 37 elabg ⊢ ( 𝐹 ∈ 𝑍 → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ↔ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
39 38 3ad2ant3 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ↔ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
40 f1oeq23 ⊢ ( ( 𝑉 = ( Vtx ‘ 𝐺 ) ∧ 𝑊 = ( Vtx ‘ 𝐻 ) ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ↔ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) )
41 1 2 40 mp2an ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ↔ 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) )
42 1 raleqi ⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ↔ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) )
43 41 42 anbi12i ⊢ ( ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ↔ ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) )
44 39 43 bitr4di ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )
45 30 44 bitrd ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) ) ) )