Theorem gricen

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

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

Proof

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