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 ⊢ · ˙ = ⋅ G
cycsubm.f ⊢ F = x ∈ ℕ 0 ⟼ x · ˙ A
cycsubm.c ⊢ C = ran ⁡ F
Assertion cycsubmel ⊢ X ∈ C ↔ ∃ i ∈ ℕ 0 X = i · ˙ A

Proof

Step Hyp Ref Expression
1 cycsubm.b ⊢ B = Base G
2 cycsubm.t ⊢ · ˙ = ⋅ G
3 cycsubm.f ⊢ F = x ∈ ℕ 0 ⟼ x · ˙ A
4 cycsubm.c ⊢ C = ran ⁡ F
5 4 eleq2i ⊢ X ∈ C ↔ X ∈ ran ⁡ F
6 ovex ⊢ x · ˙ A ∈ V
7 6 3 fnmpti ⊢ F Fn ℕ 0
8 fvelrnb ⊢ F Fn ℕ 0 → X ∈ ran ⁡ F ↔ ∃ i ∈ ℕ 0 F ⁡ i = X
9 7 8 ax-mp ⊢ X ∈ ran ⁡ F ↔ ∃ i ∈ ℕ 0 F ⁡ i = X
10 oveq1 ⊢ x = i → x · ˙ A = i · ˙ A
11 ovex ⊢ i · ˙ A ∈ V
12 10 3 11 fvmpt ⊢ i ∈ ℕ 0 → F ⁡ i = i · ˙ A
13 12 eqeq1d ⊢ i ∈ ℕ 0 → F ⁡ i = X ↔ i · ˙ A = X
14 eqcom ⊢ i · ˙ A = X ↔ X = i · ˙ A
15 13 14 bitrdi ⊢ i ∈ ℕ 0 → F ⁡ i = X ↔ X = i · ˙ A
16 15 rexbiia ⊢ ∃ i ∈ ℕ 0 F ⁡ i = X ↔ ∃ i ∈ ℕ 0 X = i · ˙ A
17 5 9 16 3bitri ⊢ X ∈ C ↔ ∃ i ∈ ℕ 0 X = i · ˙ A