Theorem brgric

Description: The relation "is isomorphic to" for graphs. (Contributed by AV, 28-Apr-2025)

	Ref	Expression
Assertion	brgric	$$⊢R{\simeq }_{𝑔𝑟}S\leftrightarrow R\mathrm{GraphIso}S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-gric	$$⊢{\simeq }_{𝑔𝑟}={\mathrm{GraphIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		grimfn	$$⊢\mathrm{GraphIso}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
3	1 2	brwitnlem	$$⊢R{\simeq }_{𝑔𝑟}S\leftrightarrow R\mathrm{GraphIso}S\ne \varnothing$$