Theorem brgrici

Description: Prove that two graphs are isomorphic by an explicit isomorphism. (Contributed by AV, 28-Apr-2025)

	Ref	Expression
Assertion	brgrici	$$⊢F\in \left(R\mathrm{GraphIso}S\right)\to R{\simeq }_{𝑔𝑟}S$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢F\in \left(R\mathrm{GraphIso}S\right)\to R\mathrm{GraphIso}S\ne \varnothing$$
2		brgric	$$⊢R{\simeq }_{𝑔𝑟}S\leftrightarrow R\mathrm{GraphIso}S\ne \varnothing$$
3	1 2	sylibr	$$⊢F\in \left(R\mathrm{GraphIso}S\right)\to R{\simeq }_{𝑔𝑟}S$$