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={\mathrm{Base}}_G$$
	cycsubm.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	cycsubm.f	$$⊢F=\left(x\in {\mathbb{N}}_0⟼x\underset{\dot{}}{·}A\right)$$
	cycsubm.c	$$⊢C=\mathrm{ran}F$$
Assertion	cycsubmel	$$⊢X\in C\leftrightarrow \exists i\in {\mathbb{N}}_{0}X=i\underset{\dot{}}{·}A$$

Proof

Step	Hyp	Ref	Expression
1		cycsubm.b	$$⊢B={\mathrm{Base}}_G$$
2		cycsubm.t	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		cycsubm.f	$$⊢F=\left(x\in {\mathbb{N}}_0⟼x\underset{\dot{}}{·}A\right)$$
4		cycsubm.c	$$⊢C=\mathrm{ran}F$$
5	4	eleq2i	$$⊢X\in C\leftrightarrow X\in \mathrm{ran}F$$
6		ovex	$$⊢x\underset{\dot{}}{·}A\in \mathrm{V}$$
7	6 3	fnmpti	$$⊢FFn{\mathbb{N}}_0$$
8		fvelrnb	$$⊢FFn{\mathbb{N}}_0\to \left(X\in \mathrm{ran}F\leftrightarrow \exists i\in {\mathbb{N}}_{0}F\left(i\right)=X\right)$$
9	7 8	ax-mp	$$⊢X\in \mathrm{ran}F\leftrightarrow \exists i\in {\mathbb{N}}_{0}F\left(i\right)=X$$
10		oveq1	$$⊢x=i\to x\underset{\dot{}}{·}A=i\underset{\dot{}}{·}A$$
11		ovex	$$⊢i\underset{\dot{}}{·}A\in \mathrm{V}$$
12	10 3 11	fvmpt	$$⊢i\in {\mathbb{N}}_0\to F\left(i\right)=i\underset{\dot{}}{·}A$$
13	12	eqeq1d	$$⊢i\in {\mathbb{N}}_0\to \left(F\left(i\right)=X\leftrightarrow i\underset{\dot{}}{·}A=X\right)$$
14		eqcom	$$⊢i\underset{\dot{}}{·}A=X\leftrightarrow X=i\underset{\dot{}}{·}A$$
15	13 14	bitrdi	$$⊢i\in {\mathbb{N}}_0\to \left(F\left(i\right)=X\leftrightarrow X=i\underset{\dot{}}{·}A\right)$$
16	15	rexbiia	$$⊢\exists i\in {\mathbb{N}}_{0}F\left(i\right)=X\leftrightarrow \exists i\in {\mathbb{N}}_{0}X=i\underset{\dot{}}{·}A$$
17	5 9 16	3bitri	$$⊢X\in C\leftrightarrow \exists i\in {\mathbb{N}}_{0}X=i\underset{\dot{}}{·}A$$