Theorem grlicen

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

	Ref	Expression
Hypotheses	grlicen.b	⊢ 𝐵 = ( Vtx ‘ 𝑅 )
	grlicen.c	⊢ 𝐶 = ( Vtx ‘ 𝑆 )
Assertion	grlicen	⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		grlicen.b	⊢ 𝐵 = ( Vtx ‘ 𝑅 )
2		grlicen.c	⊢ 𝐶 = ( Vtx ‘ 𝑆 )
3		brgrlic	⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ )
4		n0	⊢ ( ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) )
5	1 2	grlimf1o	⊢ ( 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) → 𝑓 : 𝐵 –1-1-onto→ 𝐶 )
6	1	fvexi	⊢ 𝐵 ∈ V
7	6	f1oen	⊢ ( 𝑓 : 𝐵 –1-1-onto→ 𝐶 → 𝐵 ≈ 𝐶 )
8	5 7	syl	⊢ ( 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) → 𝐵 ≈ 𝐶 )
9	8	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 GraphLocIso 𝑆 ) → 𝐵 ≈ 𝐶 )
10	4 9	sylbi	⊢ ( ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ → 𝐵 ≈ 𝐶 )
11	3 10	sylbi	⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 → 𝐵 ≈ 𝐶 )