Theorem cycsubmel

Description: Characterization of an element of the set of nonnegative integer powers of an element 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	cycsubmel	|- ( X e. C <-> E. i e. NN0 X = ( i .x. A ) )

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	4	eleq2i	|- ( X e. C <-> X e. ran F )
6		ovex	|- ( x .x. A ) e. _V
7	6 3	fnmpti	|- F Fn NN0
8		fvelrnb	|- ( F Fn NN0 -> ( X e. ran F <-> E. i e. NN0 ( F ` i ) = X ) )
9	7 8	ax-mp	|- ( X e. ran F <-> E. i e. NN0 ( F ` i ) = X )
10		oveq1	|- ( x = i -> ( x .x. A ) = ( i .x. A ) )
11		ovex	|- ( i .x. A ) e. _V
12	10 3 11	fvmpt	|- ( i e. NN0 -> ( F ` i ) = ( i .x. A ) )
13	12	eqeq1d	|- ( i e. NN0 -> ( ( F ` i ) = X <-> ( i .x. A ) = X ) )
14		eqcom	|- ( ( i .x. A ) = X <-> X = ( i .x. A ) )
15	13 14	bitrdi	|- ( i e. NN0 -> ( ( F ` i ) = X <-> X = ( i .x. A ) ) )
16	15	rexbiia	|- ( E. i e. NN0 ( F ` i ) = X <-> E. i e. NN0 X = ( i .x. A ) )
17	5 9 16	3bitri	|- ( X e. C <-> E. i e. NN0 X = ( i .x. A ) )