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 ⊢ 𝐵 = ( 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 𝑋 = ( 𝑖 · 𝐴 ) )