Metamath Proof Explorer

Theorem grilcbri2

Description: Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025)

Ref Expression
Hypotheses dfgrlic2.v ⊢ V = Vtx ⁡ G
dfgrlic2.w ⊢ W = Vtx ⁡ H
dfgrlic3.i ⊢ I = iEdg ⁡ G
dfgrlic3.j ⊢ J = iEdg ⁡ H
grilcbri2.n ⊢ N = G ClNeighbVtx X
grilcbri2.m ⊢ M = H ClNeighbVtx f ⁡ X
grilcbri2.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
grilcbri2.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
Assertion grilcbri2 ⊢ G ≃ 𝑙𝑔𝑟 H → ∃ f f : V ⟶ 1-1 onto W ∧ X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i

Proof

Step Hyp Ref Expression
1 dfgrlic2.v ⊢ V = Vtx ⁡ G
2 dfgrlic2.w ⊢ W = Vtx ⁡ H
3 dfgrlic3.i ⊢ I = iEdg ⁡ G
4 dfgrlic3.j ⊢ J = iEdg ⁡ H
5 grilcbri2.n ⊢ N = G ClNeighbVtx X
6 grilcbri2.m ⊢ M = H ClNeighbVtx f ⁡ X
7 grilcbri2.k ⊢ K = x ∈ dom ⁡ I | I ⁡ x ⊆ N
8 grilcbri2.l ⊢ L = x ∈ dom ⁡ J | J ⁡ x ⊆ M
9 brgrlic ⊢ G ≃ 𝑙𝑔𝑟 H ↔ G GraphLocIso H ≠ ∅
10 grlimdmrel ⊢ Rel ⁡ dom ⁡ GraphLocIso
11 10 ovprc ⊢ ¬ G ∈ V ∧ H ∈ V → G GraphLocIso H = ∅
12 11 necon1ai ⊢ G GraphLocIso H ≠ ∅ → G ∈ V ∧ H ∈ V
13 9 12 sylbi ⊢ G ≃ 𝑙𝑔𝑟 H → G ∈ V ∧ H ∈ V
14 eqid ⊢ G ClNeighbVtx v = G ClNeighbVtx v
15 eqid ⊢ H ClNeighbVtx f ⁡ v = H ClNeighbVtx f ⁡ v
16 eqid ⊢ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v = x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v
17 eqid ⊢ x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v = x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v
18 1 2 3 4 14 15 16 17 dfgrlic3 ⊢ G ∈ V ∧ H ∈ V → G ≃ 𝑙𝑔𝑟 H ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i
19 eqidd ⊢ v = X → j = j
20 oveq2 ⊢ v = X → G ClNeighbVtx v = G ClNeighbVtx X
21 20 5 eqtr4di ⊢ v = X → G ClNeighbVtx v = N
22 fveq2 ⊢ v = X → f ⁡ v = f ⁡ X
23 22 oveq2d ⊢ v = X → H ClNeighbVtx f ⁡ v = H ClNeighbVtx f ⁡ X
24 23 6 eqtr4di ⊢ v = X → H ClNeighbVtx f ⁡ v = M
25 19 21 24 f1oeq123d ⊢ v = X → j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ↔ j : N ⟶ 1-1 onto M
26 eqidd ⊢ v = X → g = g
27 21 sseq2d ⊢ v = X → I ⁡ x ⊆ G ClNeighbVtx v ↔ I ⁡ x ⊆ N
28 27 rabbidv ⊢ v = X → x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v = x ∈ dom ⁡ I | I ⁡ x ⊆ N
29 28 7 eqtr4di ⊢ v = X → x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v = K
30 24 sseq2d ⊢ v = X → J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ↔ J ⁡ x ⊆ M
31 30 rabbidv ⊢ v = X → x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v = x ∈ dom ⁡ J | J ⁡ x ⊆ M
32 31 8 eqtr4di ⊢ v = X → x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v = L
33 26 29 32 f1oeq123d ⊢ v = X → g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ↔ g : K ⟶ 1-1 onto L
34 29 raleqdv ⊢ v = X → ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i ↔ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
35 33 34 anbi12d ⊢ v = X → g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i ↔ g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
36 35 exbidv ⊢ v = X → ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i ↔ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
37 25 36 anbi12d ⊢ v = X → j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i ↔ j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
38 37 exbidv ⊢ v = X → ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i ↔ ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
39 38 rspcv ⊢ X ∈ V → ∀ v ∈ V ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
40 39 com12 ⊢ ∀ v ∈ V ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i → X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
41 40 a1i ⊢ G ∈ V ∧ H ∈ V → ∀ v ∈ V ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i → X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
42 41 anim2d ⊢ G ∈ V ∧ H ∈ V → f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i → f : V ⟶ 1-1 onto W ∧ X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
43 42 eximdv ⊢ G ∈ V ∧ H ∈ V → ∃ f f : V ⟶ 1-1 onto W ∧ ∀ v ∈ V ∃ j j : G ClNeighbVtx v ⟶ 1-1 onto H ClNeighbVtx f ⁡ v ∧ ∃ g g : x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v ⟶ 1-1 onto x ∈ dom ⁡ J | J ⁡ x ⊆ H ClNeighbVtx f ⁡ v ∧ ∀ i ∈ x ∈ dom ⁡ I | I ⁡ x ⊆ G ClNeighbVtx v j I ⁡ i = J ⁡ g ⁡ i → ∃ f f : V ⟶ 1-1 onto W ∧ X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
44 18 43 sylbid ⊢ G ∈ V ∧ H ∈ V → G ≃ 𝑙𝑔𝑟 H → ∃ f f : V ⟶ 1-1 onto W ∧ X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i
45 13 44 mpcom ⊢ G ≃ 𝑙𝑔𝑟 H → ∃ f f : V ⟶ 1-1 onto W ∧ X ∈ V → ∃ j j : N ⟶ 1-1 onto M ∧ ∃ g g : K ⟶ 1-1 onto L ∧ ∀ i ∈ K j I ⁡ i = J ⁡ g ⁡ i