giccyg

Description: Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016)

		Ref	Expression
	Assertion	giccyg	$⊢ G ≃_{𝑔} H \to (G \in CycGrp \to H \in CycGrp)$

Step	Hyp	Ref	Expression
1		brgic	$⊢ G ≃_{𝑔} H \leftrightarrow G GrpIso H \neq \emptyset$
2		n0	$⊢ G GrpIso H \neq \emptyset \leftrightarrow \exists f f \in (G GrpIso H)$
3		gimghm	$⊢ f \in (G GrpIso H) \to f \in (G GrpHom H)$
4		eqid	$⊢ {Base}_{G} = {Base}_{G}$
5		eqid	$⊢ {Base}_{H} = {Base}_{H}$
6	4 5	gimf1o	$⊢ f \in (G GrpIso H) \to f : {Base}_{G} \underset{1-1 onto}{⟶} {Base}_{H}$
7		f1ofo	$⊢ f : {Base}_{G} \underset{1-1 onto}{⟶} {Base}_{H} \to f : {Base}_{G} \underset{onto}{⟶} {Base}_{H}$
8	6 7	syl	$⊢ f \in (G GrpIso H) \to f : {Base}_{G} \underset{onto}{⟶} {Base}_{H}$
9	4 5	ghmcyg	$⊢ (f \in (G GrpHom H) \land f : {Base}_{G} \underset{onto}{⟶} {Base}_{H}) \to (G \in CycGrp \to H \in CycGrp)$
10	3 8 9	syl2anc	$⊢ f \in (G GrpIso H) \to (G \in CycGrp \to H \in CycGrp)$
11	10	exlimiv	$⊢ \exists f f \in (G GrpIso H) \to (G \in CycGrp \to H \in CycGrp)$
12	2 11	sylbi	$⊢ G GrpIso H \neq \emptyset \to (G \in CycGrp \to H \in CycGrp)$
13	1 12	sylbi	$⊢ G ≃_{𝑔} H \to (G \in CycGrp \to H \in CycGrp)$

Metamath Proof Explorer