Theorem gicen

Description: Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015)

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

Proof

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