Theorem frgpcyg

Description: A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016) (Proof shortened by AV, 18-Apr-2021)

	Ref	Expression
Hypothesis	frgpcyg.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
Assertion	frgpcyg	⊢ ( 𝐼 ≼ 1o ↔ 𝐺 ∈ CycGrp )

Proof

Step	Hyp	Ref	Expression
1		frgpcyg.g	⊢ 𝐺 = ( freeGrp ‘ 𝐼 )
2		brdom2	⊢ ( 𝐼 ≼ 1o ↔ ( 𝐼 ≺ 1o ∨ 𝐼 ≈ 1o ) )
3		sdom1	⊢ ( 𝐼 ≺ 1o ↔ 𝐼 = ∅ )
4		fveq2	⊢ ( 𝐼 = ∅ → ( freeGrp ‘ 𝐼 ) = ( freeGrp ‘ ∅ ) )
5	1 4	syl5eq	⊢ ( 𝐼 = ∅ → 𝐺 = ( freeGrp ‘ ∅ ) )
6		0ex	⊢ ∅ ∈ V
7		eqid	⊢ ( freeGrp ‘ ∅ ) = ( freeGrp ‘ ∅ )
8	7	frgpgrp	⊢ ( ∅ ∈ V → ( freeGrp ‘ ∅ ) ∈ Grp )
9	6 8	ax-mp	⊢ ( freeGrp ‘ ∅ ) ∈ Grp
10		eqid	⊢ ( Base ‘ ( freeGrp ‘ ∅ ) ) = ( Base ‘ ( freeGrp ‘ ∅ ) )
11	7 10	0frgp	⊢ ( Base ‘ ( freeGrp ‘ ∅ ) ) ≈ 1o
12	10	0cyg	⊢ ( ( ( freeGrp ‘ ∅ ) ∈ Grp ∧ ( Base ‘ ( freeGrp ‘ ∅ ) ) ≈ 1o ) → ( freeGrp ‘ ∅ ) ∈ CycGrp )
13	9 11 12	mp2an	⊢ ( freeGrp ‘ ∅ ) ∈ CycGrp
14	5 13	eqeltrdi	⊢ ( 𝐼 = ∅ → 𝐺 ∈ CycGrp )
15	3 14	sylbi	⊢ ( 𝐼 ≺ 1o → 𝐺 ∈ CycGrp )
16		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
17		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
18		relen	⊢ Rel ≈
19	18	brrelex1i	⊢ ( 𝐼 ≈ 1o → 𝐼 ∈ V )
20	1	frgpgrp	⊢ ( 𝐼 ∈ V → 𝐺 ∈ Grp )
21	19 20	syl	⊢ ( 𝐼 ≈ 1o → 𝐺 ∈ Grp )
22		eqid	⊢ ( ~FG ‘ 𝐼 ) = ( ~FG ‘ 𝐼 )
23		eqid	⊢ ( varFGrp ‘ 𝐼 ) = ( varFGrp ‘ 𝐼 )
24	22 23 1 16	vrgpf	⊢ ( 𝐼 ∈ V → ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
25	19 24	syl	⊢ ( 𝐼 ≈ 1o → ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
26		en1uniel	⊢ ( 𝐼 ≈ 1o → ∪ 𝐼 ∈ 𝐼 )
27	25 26	ffvelrnd	⊢ ( 𝐼 ≈ 1o → ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ∈ ( Base ‘ 𝐺 ) )
28		zringgrp	⊢ ℤring ∈ Grp
29	19	uniexd	⊢ ( 𝐼 ≈ 1o → ∪ 𝐼 ∈ V )
30		1zzd	⊢ ( 𝐼 ≈ 1o → 1 ∈ ℤ )
31	29 30	fsnd	⊢ ( 𝐼 ≈ 1o → { ⟨ ∪ 𝐼 , 1 ⟩ } : { ∪ 𝐼 } ⟶ ℤ )
32		en1b	⊢ ( 𝐼 ≈ 1o ↔ 𝐼 = { ∪ 𝐼 } )
33	32	biimpi	⊢ ( 𝐼 ≈ 1o → 𝐼 = { ∪ 𝐼 } )
34	33	feq2d	⊢ ( 𝐼 ≈ 1o → ( { ⟨ ∪ 𝐼 , 1 ⟩ } : 𝐼 ⟶ ℤ ↔ { ⟨ ∪ 𝐼 , 1 ⟩ } : { ∪ 𝐼 } ⟶ ℤ ) )
35	31 34	mpbird	⊢ ( 𝐼 ≈ 1o → { ⟨ ∪ 𝐼 , 1 ⟩ } : 𝐼 ⟶ ℤ )
36		zringbas	⊢ ℤ = ( Base ‘ ℤring )
37	1 36 23	frgpup3	⊢ ( ( ℤring ∈ Grp ∧ 𝐼 ∈ V ∧ { ⟨ ∪ 𝐼 , 1 ⟩ } : 𝐼 ⟶ ℤ ) → ∃! 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } )
38	28 19 35 37	mp3an2i	⊢ ( 𝐼 ≈ 1o → ∃! 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } )
39	38	adantr	⊢ ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ∃! 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } )
40		reurex	⊢ ( ∃! 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } → ∃ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } )
41	39 40	syl	⊢ ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ∃ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } )
42		fveq1	⊢ ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } → ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) ‘ ∪ 𝐼 ) = ( { ⟨ ∪ 𝐼 , 1 ⟩ } ‘ ∪ 𝐼 ) )
43	25 26	fvco3d	⊢ ( 𝐼 ≈ 1o → ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) ‘ ∪ 𝐼 ) = ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
44		1z	⊢ 1 ∈ ℤ
45		fvsng	⊢ ( ( ∪ 𝐼 ∈ V ∧ 1 ∈ ℤ ) → ( { ⟨ ∪ 𝐼 , 1 ⟩ } ‘ ∪ 𝐼 ) = 1 )
46	29 44 45	sylancl	⊢ ( 𝐼 ≈ 1o → ( { ⟨ ∪ 𝐼 , 1 ⟩ } ‘ ∪ 𝐼 ) = 1 )
47	43 46	eqeq12d	⊢ ( 𝐼 ≈ 1o → ( ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) ‘ ∪ 𝐼 ) = ( { ⟨ ∪ 𝐼 , 1 ⟩ } ‘ ∪ 𝐼 ) ↔ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) )
48	42 47	syl5ib	⊢ ( 𝐼 ≈ 1o → ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } → ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) )
49	48	ad2antrr	⊢ ( ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ) → ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } → ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) )
50	16 36	ghmf	⊢ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) → 𝑓 : ( Base ‘ 𝐺 ) ⟶ ℤ )
51	50	ad2antrl	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → 𝑓 : ( Base ‘ 𝐺 ) ⟶ ℤ )
52	51	ffvelrnda	⊢ ( ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℤ )
53	52	an32s	⊢ ( ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑓 ‘ 𝑥 ) ∈ ℤ )
54		mptresid	⊢ ( I ↾ ( Base ‘ 𝐺 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 )
55	1 16 23	frgpup3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝐼 ∈ V ∧ ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) ) → ∃! 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
56	21 19 25 55	syl3anc	⊢ ( 𝐼 ≈ 1o → ∃! 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
57		reurmo	⊢ ( ∃! 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) → ∃* 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
58	56 57	syl	⊢ ( 𝐼 ≈ 1o → ∃* 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
59	58	adantr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ∃* 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
60	21	adantr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → 𝐺 ∈ Grp )
61	16	idghm	⊢ ( 𝐺 ∈ Grp → ( I ↾ ( Base ‘ 𝐺 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) )
62	60 61	syl	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( I ↾ ( Base ‘ 𝐺 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) )
63	25	adantr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) )
64		fcoi2	⊢ ( ( varFGrp ‘ 𝐼 ) : 𝐼 ⟶ ( Base ‘ 𝐺 ) → ( ( I ↾ ( Base ‘ 𝐺 ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
65	63 64	syl	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( I ↾ ( Base ‘ 𝐺 ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
66	51	feqmptd	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → 𝑓 = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( 𝑓 ‘ 𝑥 ) ) )
67		eqidd	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
68		oveq1	⊢ ( 𝑛 = ( 𝑓 ‘ 𝑥 ) → ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
69	52 66 67 68	fmptco	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ 𝑓 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
70	27	adantr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ∈ ( Base ‘ 𝐺 ) )
71		eqid	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) = ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
72	17 71 16	mulgghm2	⊢ ( ( 𝐺 ∈ Grp ∧ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ∈ ( Base ‘ 𝐺 ) ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∈ ( ℤring GrpHom 𝐺 ) )
73	60 70 72	syl2anc	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∈ ( ℤring GrpHom 𝐺 ) )
74		simprl	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → 𝑓 ∈ ( 𝐺 GrpHom ℤring ) )
75		ghmco	⊢ ( ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∈ ( ℤring GrpHom 𝐺 ) ∧ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ) → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ 𝑓 ) ∈ ( 𝐺 GrpHom 𝐺 ) )
76	73 74 75	syl2anc	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ 𝑓 ) ∈ ( 𝐺 GrpHom 𝐺 ) )
77	69 76	eqeltrrd	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∈ ( 𝐺 GrpHom 𝐺 ) )
78	33	adantr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → 𝐼 = { ∪ 𝐼 } )
79	78	eleq2d	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑦 ∈ 𝐼 ↔ 𝑦 ∈ { ∪ 𝐼 } ) )
80		simprr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 )
81	80	oveq1d	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( 1 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
82	16 17	mulg1	⊢ ( ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ∈ ( Base ‘ 𝐺 ) → ( 1 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) )
83	70 82	syl	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 1 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) )
84	81 83	eqtrd	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) )
85		elsni	⊢ ( 𝑦 ∈ { ∪ 𝐼 } → 𝑦 = ∪ 𝐼 )
86	85	fveq2d	⊢ ( 𝑦 ∈ { ∪ 𝐼 } → ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) = ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) )
87	86	fveq2d	⊢ ( 𝑦 ∈ { ∪ 𝐼 } → ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) = ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
88	87	oveq1d	⊢ ( 𝑦 ∈ { ∪ 𝐼 } → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
89	88 86	eqeq12d	⊢ ( 𝑦 ∈ { ∪ 𝐼 } → ( ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ↔ ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
90	84 89	syl5ibrcom	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑦 ∈ { ∪ 𝐼 } → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) )
91	79 90	sylbid	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑦 ∈ 𝐼 → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) )
92	91	imp	⊢ ( ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) )
93	92	mpteq2dva	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) )
94	63	ffvelrnda	⊢ ( ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) ∧ 𝑦 ∈ 𝐼 ) → ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐺 ) )
95	63	feqmptd	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( varFGrp ‘ 𝐼 ) = ( 𝑦 ∈ 𝐼 ↦ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) )
96		eqidd	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
97		fveq2	⊢ ( 𝑥 = ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) )
98	97	oveq1d	⊢ ( 𝑥 = ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) → ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
99	94 95 96 98	fmptco	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( 𝑦 ∈ 𝐼 ↦ ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ 𝑦 ) ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
100	93 99 95	3eqtr4d	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) )
101		coeq1	⊢ ( 𝑔 = ( I ↾ ( Base ‘ 𝐺 ) ) → ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( ( I ↾ ( Base ‘ 𝐺 ) ) ∘ ( varFGrp ‘ 𝐼 ) ) )
102	101	eqeq1d	⊢ ( 𝑔 = ( I ↾ ( Base ‘ 𝐺 ) ) → ( ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ↔ ( ( I ↾ ( Base ‘ 𝐺 ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ) )
103		coeq1	⊢ ( 𝑔 = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) → ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ ( varFGrp ‘ 𝐼 ) ) )
104	103	eqeq1d	⊢ ( 𝑔 = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) → ( ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ) )
105	102 104	rmoi	⊢ ( ( ∃* 𝑔 ∈ ( 𝐺 GrpHom 𝐺 ) ( 𝑔 ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ∧ ( ( I ↾ ( Base ‘ 𝐺 ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( ( I ↾ ( Base ‘ 𝐺 ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ) ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∈ ( 𝐺 GrpHom 𝐺 ) ∧ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ∘ ( varFGrp ‘ 𝐼 ) ) = ( varFGrp ‘ 𝐼 ) ) ) → ( I ↾ ( Base ‘ 𝐺 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
106	59 62 65 77 100 105	syl122anc	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( I ↾ ( Base ‘ 𝐺 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
107	54 106	syl5eqr	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
108		mpteqb	⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑥 ∈ ( Base ‘ 𝐺 ) → ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑥 = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
109		id	⊢ ( 𝑥 ∈ ( Base ‘ 𝐺 ) → 𝑥 ∈ ( Base ‘ 𝐺 ) )
110	108 109	mprg	⊢ ( ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ 𝑥 ) = ( 𝑥 ∈ ( Base ‘ 𝐺 ) ↦ ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑥 = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
111	107 110	sylib	⊢ ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) 𝑥 = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
112	111	r19.21bi	⊢ ( ( ( 𝐼 ≈ 1o ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
113	112	an32s	⊢ ( ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → 𝑥 = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
114	68	rspceeqv	⊢ ( ( ( 𝑓 ‘ 𝑥 ) ∈ ℤ ∧ 𝑥 = ( ( 𝑓 ‘ 𝑥 ) ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
115	53 113 114	syl2anc	⊢ ( ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ ( 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ∧ ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 ) ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
116	115	expr	⊢ ( ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ) → ( ( 𝑓 ‘ ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) = 1 → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
117	49 116	syld	⊢ ( ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) ∧ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ) → ( ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
118	117	rexlimdva	⊢ ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ∃ 𝑓 ∈ ( 𝐺 GrpHom ℤring ) ( 𝑓 ∘ ( varFGrp ‘ 𝐼 ) ) = { ⟨ ∪ 𝐼 , 1 ⟩ } → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) ) )
119	41 118	mpd	⊢ ( ( 𝐼 ≈ 1o ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ∃ 𝑛 ∈ ℤ 𝑥 = ( 𝑛 ( .g ‘ 𝐺 ) ( ( varFGrp ‘ 𝐼 ) ‘ ∪ 𝐼 ) ) )
120	16 17 21 27 119	iscygd	⊢ ( 𝐼 ≈ 1o → 𝐺 ∈ CycGrp )
121	15 120	jaoi	⊢ ( ( 𝐼 ≺ 1o ∨ 𝐼 ≈ 1o ) → 𝐺 ∈ CycGrp )
122	2 121	sylbi	⊢ ( 𝐼 ≼ 1o → 𝐺 ∈ CycGrp )
123		cygabl	⊢ ( 𝐺 ∈ CycGrp → 𝐺 ∈ Abel )
124	1	frgpnabl	⊢ ( 1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel )
125	124	con2i	⊢ ( 𝐺 ∈ Abel → ¬ 1o ≺ 𝐼 )
126		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
127		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
128	16 127	grpidcl	⊢ ( 𝐺 ∈ Grp → ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) )
129	1 16	elbasfv	⊢ ( ( 0g ‘ 𝐺 ) ∈ ( Base ‘ 𝐺 ) → 𝐼 ∈ V )
130	126 128 129	3syl	⊢ ( 𝐺 ∈ Abel → 𝐼 ∈ V )
131		1onn	⊢ 1o ∈ ω
132		nnfi	⊢ ( 1o ∈ ω → 1o ∈ Fin )
133	131 132	ax-mp	⊢ 1o ∈ Fin
134		fidomtri2	⊢ ( ( 𝐼 ∈ V ∧ 1o ∈ Fin ) → ( 𝐼 ≼ 1o ↔ ¬ 1o ≺ 𝐼 ) )
135	130 133 134	sylancl	⊢ ( 𝐺 ∈ Abel → ( 𝐼 ≼ 1o ↔ ¬ 1o ≺ 𝐼 ) )
136	125 135	mpbird	⊢ ( 𝐺 ∈ Abel → 𝐼 ≼ 1o )
137	123 136	syl	⊢ ( 𝐺 ∈ CycGrp → 𝐼 ≼ 1o )
138	122 137	impbii	⊢ ( 𝐼 ≼ 1o ↔ 𝐺 ∈ CycGrp )