Metamath Proof Explorer

Theorem grlicref

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

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

Proof

Step Hyp Ref Expression
1 fvexd ⊢ G ∈ UHGraph → Vtx ⁡ G ∈ V
2 1 resiexd ⊢ G ∈ UHGraph → I ↾ Vtx ⁡ G ∈ V
3 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
4 3 clnbgrssvtx ⊢ G ClNeighbVtx v ⊆ Vtx ⁡ G
5 4 a1i ⊢ v ∈ Vtx ⁡ G → G ClNeighbVtx v ⊆ Vtx ⁡ G
6 3 isubgruhgr ⊢ G ∈ UHGraph ∧ G ClNeighbVtx v ⊆ Vtx ⁡ G → G ISubGr G ClNeighbVtx v ∈ UHGraph
7 5 6 sylan2 ⊢ G ∈ UHGraph ∧ v ∈ Vtx ⁡ G → G ISubGr G ClNeighbVtx v ∈ UHGraph
8 gricref ⊢ G ISubGr G ClNeighbVtx v ∈ UHGraph → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
9 7 8 syl ⊢ G ∈ UHGraph ∧ v ∈ Vtx ⁡ G → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
10 9 ralrimiva ⊢ G ∈ UHGraph → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
11 f1oi ⊢ I ↾ Vtx ⁡ G : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G
12 10 11 jctil ⊢ G ∈ UHGraph → I ↾ Vtx ⁡ G : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
13 f1oeq1 ⊢ f = I ↾ Vtx ⁡ G → f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ↔ I ↾ Vtx ⁡ G : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G
14 fveq1 ⊢ f = I ↾ Vtx ⁡ G → f ⁡ v = I ↾ Vtx ⁡ G ⁡ v
15 14 oveq2d ⊢ f = I ↾ Vtx ⁡ G → G ClNeighbVtx f ⁡ v = G ClNeighbVtx I ↾ Vtx ⁡ G ⁡ v
16 15 oveq2d ⊢ f = I ↾ Vtx ⁡ G → G ISubGr G ClNeighbVtx f ⁡ v = G ISubGr G ClNeighbVtx I ↾ Vtx ⁡ G ⁡ v
17 16 breq2d ⊢ f = I ↾ Vtx ⁡ G → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v ↔ G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx I ↾ Vtx ⁡ G ⁡ v
18 fvresi ⊢ v ∈ Vtx ⁡ G → I ↾ Vtx ⁡ G ⁡ v = v
19 18 oveq2d ⊢ v ∈ Vtx ⁡ G → G ClNeighbVtx I ↾ Vtx ⁡ G ⁡ v = G ClNeighbVtx v
20 19 oveq2d ⊢ v ∈ Vtx ⁡ G → G ISubGr G ClNeighbVtx I ↾ Vtx ⁡ G ⁡ v = G ISubGr G ClNeighbVtx v
21 20 breq2d ⊢ v ∈ Vtx ⁡ G → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx I ↾ Vtx ⁡ G ⁡ v ↔ G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
22 17 21 sylan9bb ⊢ f = I ↾ Vtx ⁡ G ∧ v ∈ Vtx ⁡ G → G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v ↔ G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
23 22 ralbidva ⊢ f = I ↾ Vtx ⁡ G → ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v ↔ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
24 13 23 anbi12d ⊢ f = I ↾ Vtx ⁡ G → f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v ↔ I ↾ Vtx ⁡ G : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx v
25 2 12 24 spcedv ⊢ G ∈ UHGraph → ∃ f f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v
26 3 3 dfgrlic2 ⊢ G ∈ UHGraph ∧ G ∈ UHGraph → G ≃ 𝑙𝑔𝑟 G ↔ ∃ f f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v
27 26 anidms ⊢ G ∈ UHGraph → G ≃ 𝑙𝑔𝑟 G ↔ ∃ f f : Vtx ⁡ G ⟶ 1-1 onto Vtx ⁡ G ∧ ∀ v ∈ Vtx ⁡ G G ISubGr G ClNeighbVtx v ≃ 𝑔𝑟 G ISubGr G ClNeighbVtx f ⁡ v
28 25 27 mpbird ⊢ G ∈ UHGraph → G ≃ 𝑙𝑔𝑟 G