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 ⊢ V = Vtx ⁡ G
isgrlim.w ⊢ W = Vtx ⁡ H
Assertion isgrlim ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v

Proof

Step Hyp Ref Expression
1 isgrlim.v ⊢ V = Vtx ⁡ G
2 isgrlim.w ⊢ W = Vtx ⁡ H
3 df-grlim ⊢ GraphLocIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
4 elex ⊢ G ∈ X → G ∈ V
5 4 3ad2ant1 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → G ∈ V
6 elex ⊢ H ∈ Y → H ∈ V
7 6 3ad2ant2 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → H ∈ V
8 f1of ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H → f : Vtx ⁡ G ⟶ Vtx ⁡ H
9 8 adantr ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v → f : Vtx ⁡ G ⟶ Vtx ⁡ H
10 9 adantl ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z ∧ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v → f : Vtx ⁡ G ⟶ Vtx ⁡ H
11 fvexd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → Vtx ⁡ G ∈ V
12 fvexd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → Vtx ⁡ H ∈ V
13 10 11 12 fabexd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ∈ V
14 eqidd ⊢ g = G ∧ h = H → f = f
15 fveq2 ⊢ g = G → Vtx ⁡ g = Vtx ⁡ G
16 15 adantr ⊢ g = G ∧ h = H → Vtx ⁡ g = Vtx ⁡ G
17 fveq2 ⊢ h = H → Vtx ⁡ h = Vtx ⁡ H
18 17 adantl ⊢ g = G ∧ h = H → Vtx ⁡ h = Vtx ⁡ H
19 14 16 18 f1oeq123d ⊢ g = G ∧ h = H → f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ↔ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
20 id ⊢ g = G → g = G
21 oveq1 ⊢ g = G → g ClNeighbVtx v = G ClNeighbVtx v
22 20 21 oveq12d ⊢ g = G → g ISubGr g ClNeighbVtx v = G ISubGr G ClNeighbVtx v
23 id ⊢ h = H → h = H
24 oveq1 ⊢ h = H → h ClNeighbVtx f ⁡ v = H ClNeighbVtx f ⁡ v
25 23 24 oveq12d ⊢ h = H → h ISubGr h ClNeighbVtx f ⁡ v = H ISubGr H ClNeighbVtx f ⁡ v
26 22 25 breqan12d ⊢ g = G ∧ h = H → g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v ↔ G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
27 16 26 raleqbidv ⊢ g = G ∧ h = H → ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v ↔ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
28 19 27 anbi12d ⊢ g = G ∧ h = H → f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v ↔ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
29 28 abbidv ⊢ g = G ∧ h = H → f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v = f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
30 3 5 7 13 29 elovmpod ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v
31 f1oeq1 ⊢ f = F → f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
32 fveq1 ⊢ f = F → f ⁡ v = F ⁡ v
33 32 oveq2d ⊢ f = F → H ClNeighbVtx f ⁡ v = H ClNeighbVtx F ⁡ v
34 33 oveq2d ⊢ f = F → H ISubGr H ClNeighbVtx f ⁡ v = H ISubGr H ClNeighbVtx F ⁡ v
35 34 breq2d ⊢ f = F → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ↔ G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
36 35 ralbidv ⊢ f = F → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ↔ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
37 31 36 anbi12d ⊢ f = F → f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
38 37 elabg ⊢ F ∈ Z → F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
39 38 3ad2ant3 ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
40 f1oeq23 ⊢ V = Vtx ⁡ G ∧ W = Vtx ⁡ H → F : V ⟶ 1-1 onto W ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
41 1 2 40 mp2an ⊢ F : V ⟶ 1-1 onto W ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H
42 1 raleqi ⊢ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
43 41 42 anbi12i ⊢ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v ↔ F : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
44 39 43 bitr4di ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ f | f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ H ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx f ⁡ v ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v
45 30 44 bitrd ⊢ G ∈ X ∧ H ∈ Y ∧ F ∈ Z → F ∈ G GraphLocIso H ↔ F : V ⟶ 1-1 onto W ∧ ∀ v ∈ V G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 H ISubGr H ClNeighbVtx F ⁡ v