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

Metamath Proof Explorer

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 ) )