Metamath Proof Explorer

Theorem grlicsym

Description: Graph local isomorphism is symmetric for hypergraphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Assertion grlicsym ⊢ G ∈ UHGraph → G ≃ 𝑙𝑔𝑟 S → S ≃ 𝑙𝑔𝑟 G

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
2 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
3 1 2 grilcbri ⊢ G ≃ 𝑙𝑔𝑟 S → ∃ f f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v
4 grlicrcl ⊢ G ≃ 𝑙𝑔𝑟 S → G ∈ V ∧ S ∈ V
5 vex ⊢ f ∈ V
6 cnvexg ⊢ f ∈ V → f -1 ∈ V
7 5 6 mp1i ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph → f -1 ∈ V
8 f1ocnv ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S → f -1 : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G
9 8 ad2antrr ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph → f -1 : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G
10 f1ocnvdm ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S → f -1 ⁡ w ∈ Vtx ⁡ G
11 10 3adant3 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → f -1 ⁡ w ∈ Vtx ⁡ G
12 oveq2 ⊢ v = f -1 ⁡ w → G ClNeighbVtx v = G ClNeighbVtx f -1 ⁡ w
13 12 oveq2d ⊢ v = f -1 ⁡ w → G ISubGr G ClNeighbVtx v = G ISubGr G ClNeighbVtx f -1 ⁡ w
14 fveq2 ⊢ v = f -1 ⁡ w → f ⁡ v = f ⁡ f -1 ⁡ w
15 14 oveq2d ⊢ v = f -1 ⁡ w → S ClNeighbVtx f ⁡ v = S ClNeighbVtx f ⁡ f -1 ⁡ w
16 15 oveq2d ⊢ v = f -1 ⁡ w → S ISubGr S ClNeighbVtx f ⁡ v = S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w
17 13 16 breq12d ⊢ v = f -1 ⁡ w → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ↔ G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w
18 17 rspcv ⊢ f -1 ⁡ w ∈ Vtx ⁡ G → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w
19 11 18 syl ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w
20 f1ocnvfv2 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S → f ⁡ f -1 ⁡ w = w
21 20 3adant3 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → f ⁡ f -1 ⁡ w = w
22 21 oveq2d ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → S ClNeighbVtx f ⁡ f -1 ⁡ w = S ClNeighbVtx w
23 22 oveq2d ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w = S ISubGr S ClNeighbVtx w
24 23 breq2d ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w ↔ G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx w
25 simp3 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → G ∈ UHGraph
26 1 clnbgrssvtx ⊢ G ClNeighbVtx f -1 ⁡ w ⊆ Vtx ⁡ G
27 1 isubgruhgr ⊢ G ∈ UHGraph ∧ G ClNeighbVtx f -1 ⁡ w ⊆ Vtx ⁡ G → G ISubGr G ClNeighbVtx f -1 ⁡ w ∈ UHGraph
28 25 26 27 sylancl ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → G ISubGr G ClNeighbVtx f -1 ⁡ w ∈ UHGraph
29 gricsym ⊢ G ISubGr G ClNeighbVtx f -1 ⁡ w ∈ UHGraph → G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx w → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
30 28 29 syl ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx w → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
31 24 30 sylbid ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → G ISubGr G ClNeighbVtx f -1 ⁡ w ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ f -1 ⁡ w → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
32 19 31 syld ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ w ∈ Vtx ⁡ S ∧ G ∈ UHGraph → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
33 32 3exp ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S → w ∈ Vtx ⁡ S → G ∈ UHGraph → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
34 33 com24 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → G ∈ UHGraph → w ∈ Vtx ⁡ S → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
35 34 imp31 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph → w ∈ Vtx ⁡ S → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
36 35 ralrimiv ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph → ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
37 9 36 jca ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph → f -1 : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
38 f1oeq1 ⊢ g = f -1 → g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ↔ f -1 : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G
39 fveq1 ⊢ g = f -1 → g ⁡ w = f -1 ⁡ w
40 39 oveq2d ⊢ g = f -1 → G ClNeighbVtx g ⁡ w = G ClNeighbVtx f -1 ⁡ w
41 40 oveq2d ⊢ g = f -1 → G ISubGr G ClNeighbVtx g ⁡ w = G ISubGr G ClNeighbVtx f -1 ⁡ w
42 41 breq2d ⊢ g = f -1 → S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w ↔ S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
43 42 ralbidv ⊢ g = f -1 → ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w ↔ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
44 38 43 anbi12d ⊢ g = f -1 → g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w ↔ f -1 : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f -1 ⁡ w
45 7 37 44 spcedv ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph → ∃ g g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w
46 45 3adant3 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph ∧ G ∈ V ∧ S ∈ V → ∃ g g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w
47 2 1 dfgrlic2 ⊢ S ∈ V ∧ G ∈ V → S ≃ 𝑙𝑔𝑟 G ↔ ∃ g g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w
48 47 ancoms ⊢ G ∈ V ∧ S ∈ V → S ≃ 𝑙𝑔𝑟 G ↔ ∃ g g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w
49 48 3ad2ant3 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph ∧ G ∈ V ∧ S ∈ V → S ≃ 𝑙𝑔𝑟 G ↔ ∃ g g : Vtx ⁡ S ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ w ∈ Vtx ⁡ S S ISubGr S ClNeighbVtx w ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx g ⁡ w
50 46 49 mpbird ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v ∧ G ∈ UHGraph ∧ G ∈ V ∧ S ∈ V → S ≃ 𝑙𝑔𝑟 G
51 50 3exp ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → G ∈ UHGraph → G ∈ V ∧ S ∈ V → S ≃ 𝑙𝑔𝑟 G
52 51 com23 ⊢ f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → G ∈ V ∧ S ∈ V → G ∈ UHGraph → S ≃ 𝑙𝑔𝑟 G
53 52 exlimiv ⊢ ∃ f f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ S ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 S ISubGr S ClNeighbVtx f ⁡ v → G ∈ V ∧ S ∈ V → G ∈ UHGraph → S ≃ 𝑙𝑔𝑟 G
54 3 4 53 sylc ⊢ G ≃ 𝑙𝑔𝑟 S → G ∈ UHGraph → S ≃ 𝑙𝑔𝑟 G
55 54 com12 ⊢ G ∈ UHGraph → G ≃ 𝑙𝑔𝑟 S → S ≃ 𝑙𝑔𝑟 G