|   | Mathbox for Alexander van der Vekens | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-grlic | Structured version Visualization version GIF version | ||
| Description: Two graphs are said to be locally isomorphic iff they are connected by at least one local isomorphism. (Contributed by AV, 27-Apr-2025.) | 
| Ref | Expression | 
|---|---|
| df-grlic | ⊢ ≃𝑙𝑔𝑟 = (◡ GraphLocIso “ (V ∖ 1o)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | cgrlic 47944 | . 2 class ≃𝑙𝑔𝑟 | |
| 2 | cgrlim 47943 | . . . 4 class GraphLocIso | |
| 3 | 2 | ccnv 5684 | . . 3 class ◡ GraphLocIso | 
| 4 | cvv 3480 | . . . 4 class V | |
| 5 | c1o 8499 | . . . 4 class 1o | |
| 6 | 4, 5 | cdif 3948 | . . 3 class (V ∖ 1o) | 
| 7 | 3, 6 | cima 5688 | . 2 class (◡ GraphLocIso “ (V ∖ 1o)) | 
| 8 | 1, 7 | wceq 1540 | 1 wff ≃𝑙𝑔𝑟 = (◡ GraphLocIso “ (V ∖ 1o)) | 
| Colors of variables: wff setvar class | 
| This definition is referenced by: brgrlic 47964 grlicrel 47966 | 
| Copyright terms: Public domain | W3C validator |