Theorem grlicen

Description: Locally isomorphic graphs have equinumerous sets of vertices. (Contributed by AV, 11-Jun-2025)

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

Proof

Step	Hyp	Ref	Expression
1		grlicen.b	$$⊢B=\mathrm{Vtx}\left(R\right)$$
2		grlicen.c	$$⊢C=\mathrm{Vtx}\left(S\right)$$
3		brgrlic	$$⊢R{\simeq }_{𝑙𝑔𝑟}S\leftrightarrow R\mathrm{GraphLocIso}S\ne \varnothing$$
4		n0	$$⊢R\mathrm{GraphLocIso}S\ne \varnothing \leftrightarrow \exists ff\in \left(R\mathrm{GraphLocIso}S\right)$$
5	1 2	grlimf1o	$$⊢f\in \left(R\mathrm{GraphLocIso}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{GraphLocIso}S\right)\to B\approx C$$
9	8	exlimiv	$$⊢\exists ff\in \left(R\mathrm{GraphLocIso}S\right)\to B\approx C$$
10	4 9	sylbi	$$⊢R\mathrm{GraphLocIso}S\ne \varnothing \to B\approx C$$
11	3 10	sylbi	$$⊢R{\simeq }_{𝑙𝑔𝑟}S\to B\approx C$$