Theorem cycsubmcl

Description: The set of nonnegative integer powers of an element A contains A . Although this theorem holds for any class G , the definition of F is only meaningful if G is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023)

	Ref	Expression
Hypotheses	cycsubm.b	|- B = ( Base ` G )
	cycsubm.t	|- .x. = ( .g ` G )
	cycsubm.f	|- F = ( x e. NN0 |-> ( x .x. A ) )
	cycsubm.c	|- C = ran F
Assertion	cycsubmcl	|- ( A e. B -> A e. C )

Proof

Step	Hyp	Ref	Expression
1		cycsubm.b	|- B = ( Base ` G )
2		cycsubm.t	|- .x. = ( .g ` G )
3		cycsubm.f	|- F = ( x e. NN0 |-> ( x .x. A ) )
4		cycsubm.c	|- C = ran F
5		1nn0	|- 1 e. NN0
6	5	a1i	|- ( A e. B -> 1 e. NN0 )
7		oveq1	|- ( i = 1 -> ( i .x. A ) = ( 1 .x. A ) )
8	7	eqeq2d	|- ( i = 1 -> ( A = ( i .x. A ) <-> A = ( 1 .x. A ) ) )
9	8	adantl	|- ( ( A e. B /\ i = 1 ) -> ( A = ( i .x. A ) <-> A = ( 1 .x. A ) ) )
10	1 2	mulg1	|- ( A e. B -> ( 1 .x. A ) = A )
11	10	eqcomd	|- ( A e. B -> A = ( 1 .x. A ) )
12	6 9 11	rspcedvd	|- ( A e. B -> E. i e. NN0 A = ( i .x. A ) )
13	1 2 3 4	cycsubmel	|- ( A e. C <-> E. i e. NN0 A = ( i .x. A ) )
14	12 13	sylibr	|- ( A e. B -> A e. C )