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	⊢ 𝐵 = ( Base ‘ 𝐺 )
	cycsubm.t	⊢ · = ( .g ‘ 𝐺 )
	cycsubm.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
	cycsubm.c	⊢ 𝐶 = ran 𝐹
Assertion	cycsubmel	⊢ ( 𝑋 ∈ 𝐶 ↔ ∃ 𝑖 ∈ ℕ0 𝑋 = ( 𝑖 · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		cycsubm.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		cycsubm.t	⊢ · = ( .g ‘ 𝐺 )
3		cycsubm.f	⊢ 𝐹 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 · 𝐴 ) )
4		cycsubm.c	⊢ 𝐶 = ran 𝐹
5	4	eleq2i	⊢ ( 𝑋 ∈ 𝐶 ↔ 𝑋 ∈ ran 𝐹 )
6		ovex	⊢ ( 𝑥 · 𝐴 ) ∈ V
7	6 3	fnmpti	⊢ 𝐹 Fn ℕ0
8		fvelrnb	⊢ ( 𝐹 Fn ℕ0 → ( 𝑋 ∈ ran 𝐹 ↔ ∃ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) = 𝑋 ) )
9	7 8	ax-mp	⊢ ( 𝑋 ∈ ran 𝐹 ↔ ∃ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) = 𝑋 )
10		oveq1	⊢ ( 𝑥 = 𝑖 → ( 𝑥 · 𝐴 ) = ( 𝑖 · 𝐴 ) )
11		ovex	⊢ ( 𝑖 · 𝐴 ) ∈ V
12	10 3 11	fvmpt	⊢ ( 𝑖 ∈ ℕ0 → ( 𝐹 ‘ 𝑖 ) = ( 𝑖 · 𝐴 ) )
13	12	eqeq1d	⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑖 ) = 𝑋 ↔ ( 𝑖 · 𝐴 ) = 𝑋 ) )
14		eqcom	⊢ ( ( 𝑖 · 𝐴 ) = 𝑋 ↔ 𝑋 = ( 𝑖 · 𝐴 ) )
15	13 14	bitrdi	⊢ ( 𝑖 ∈ ℕ0 → ( ( 𝐹 ‘ 𝑖 ) = 𝑋 ↔ 𝑋 = ( 𝑖 · 𝐴 ) ) )
16	15	rexbiia	⊢ ( ∃ 𝑖 ∈ ℕ0 ( 𝐹 ‘ 𝑖 ) = 𝑋 ↔ ∃ 𝑖 ∈ ℕ0 𝑋 = ( 𝑖 · 𝐴 ) )
17	5 9 16	3bitri	⊢ ( 𝑋 ∈ 𝐶 ↔ ∃ 𝑖 ∈ ℕ0 𝑋 = ( 𝑖 · 𝐴 ) )