This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gimf1o

Description: An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015) (Revised by Mario Carneiro, 6-May-2015)

	Ref	Expression
Hypotheses	isgim.b	$⊢ B = {Base}_{R}$
	isgim.c	$⊢ C = {Base}_{S}$
Assertion	gimf1o	$⊢ F \in (R GrpIso S) \to F : B \underset{1-1 onto}{⟶} C$

Step	Hyp	Ref	Expression
1		isgim.b	$⊢ B = {Base}_{R}$
2		isgim.c	$⊢ C = {Base}_{S}$
3	1 2	isgim	$⊢ F \in (R GrpIso S) \leftrightarrow (F \in (R GrpHom S) \land F : B \underset{1-1 onto}{⟶} C)$
4	3	simprbi	$⊢ F \in (R GrpIso S) \to F : B \underset{1-1 onto}{⟶} C$