Theorem gicen

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

	Ref	Expression
Hypotheses	gicen.b	$$⊢B={\mathrm{Base}}_R$$
	gicen.c	$$⊢C={\mathrm{Base}}_S$$
Assertion	gicen	$$⊢R{\simeq }_{𝑔}S\to B\approx C$$

Proof

Step	Hyp	Ref	Expression
1		gicen.b	$$⊢B={\mathrm{Base}}_R$$
2		gicen.c	$$⊢C={\mathrm{Base}}_S$$
3		brgic	$$⊢R{\simeq }_{𝑔}S\leftrightarrow R\mathrm{GrpIso}S\ne \varnothing$$
4		n0	$$⊢R\mathrm{GrpIso}S\ne \varnothing \leftrightarrow \exists ff\in \left(R\mathrm{GrpIso}S\right)$$
5	1 2	gimf1o	$$⊢f\in \left(R\mathrm{GrpIso}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{GrpIso}S\right)\to B\approx C$$
9	8	exlimiv	$$⊢\exists ff\in \left(R\mathrm{GrpIso}S\right)\to B\approx C$$
10	4 9	sylbi	$$⊢R\mathrm{GrpIso}S\ne \varnothing \to B\approx C$$
11	3 10	sylbi	$$⊢R{\simeq }_{𝑔}S\to B\approx C$$