gicen

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

Step	Hyp	Ref	Expression
1		gicen.b	$⊢ B = {Base}_{R}$
2		gicen.c	$⊢ C = {Base}_{S}$
3		brgic	$⊢ R ≃_{𝑔} S \leftrightarrow R GrpIso S \neq \emptyset$
4		n0	$⊢ R GrpIso S \neq \emptyset \leftrightarrow \exists f f \in (R GrpIso S)$
5	1 2	gimf1o	$⊢ f \in (R GrpIso S) \to f : B \underset{1-1 onto}{⟶} C$
6	1	fvexi	$⊢ B \in V$
7	6	f1oen	$⊢ f : B \underset{1-1 onto}{⟶} C \to B \approx C$
8	5 7	syl	$⊢ f \in (R GrpIso S) \to B \approx C$
9	8	exlimiv	$⊢ \exists f f \in (R GrpIso S) \to B \approx C$
10	4 9	sylbi	$⊢ R GrpIso S \neq \emptyset \to B \approx C$
11	3 10	sylbi	$⊢ R ≃_{𝑔} S \to B \approx C$

Metamath Proof Explorer