Description: The "is isomorphic to" relation for graphs is a relation. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | gricrel | ⊢ Rel ≃𝑔𝑟 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-gric | ⊢ ≃𝑔𝑟 = ( ◡ GraphIso “ ( V ∖ 1o ) ) | |
| 2 | cnvimass | ⊢ ( ◡ GraphIso “ ( V ∖ 1o ) ) ⊆ dom GraphIso | |
| 3 | grimfn | ⊢ GraphIso Fn ( V × V ) | |
| 4 | 3 | fndmi | ⊢ dom GraphIso = ( V × V ) |
| 5 | 2 4 | sseqtri | ⊢ ( ◡ GraphIso “ ( V ∖ 1o ) ) ⊆ ( V × V ) |
| 6 | 1 5 | eqsstri | ⊢ ≃𝑔𝑟 ⊆ ( V × V ) |
| 7 | relxp | ⊢ Rel ( V × V ) | |
| 8 | relss | ⊢ ( ≃𝑔𝑟 ⊆ ( V × V ) → ( Rel ( V × V ) → Rel ≃𝑔𝑟 ) ) | |
| 9 | 6 7 8 | mp2 | ⊢ Rel ≃𝑔𝑟 |