Theorem gricen

Description: Isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 3-May-2025)

	Ref	Expression
Hypotheses	gricen.b	$$⊢B=\mathrm{Vtx}\left(R\right)$$
	gricen.c	$$⊢C=\mathrm{Vtx}\left(S\right)$$
Assertion	gricen	$$⊢R{\simeq }_{𝑔𝑟}S\to B\approx C$$

Proof

Step	Hyp	Ref	Expression
1		gricen.b	$$⊢B=\mathrm{Vtx}\left(R\right)$$
2		gricen.c	$$⊢C=\mathrm{Vtx}\left(S\right)$$
3		brgric	$$⊢R{\simeq }_{𝑔𝑟}S\leftrightarrow R\mathrm{GraphIso}S\ne \varnothing$$
4		n0	$$⊢R\mathrm{GraphIso}S\ne \varnothing \leftrightarrow \exists ff\in \left(R\mathrm{GraphIso}S\right)$$
5	1 2	grimf1o	$$⊢f\in \left(R\mathrm{GraphIso}S\right)\to f:B\underset{1-1\; onto}{⟶}C$$
6	1	fvexi	$$⊢B\in \mathrm{V}$$
7	6	f1oen	$$⊢f:B\underset{1-1\; onto}{⟶}C\to B\approx C$$
8	5 7	syl	$$⊢f\in \left(R\mathrm{GraphIso}S\right)\to B\approx C$$
9	8	exlimiv	$$⊢\exists ff\in \left(R\mathrm{GraphIso}S\right)\to B\approx C$$
10	4 9	sylbi	$$⊢R\mathrm{GraphIso}S\ne \varnothing \to B\approx C$$
11	3 10	sylbi	$$⊢R{\simeq }_{𝑔𝑟}S\to B\approx C$$