Step 
Hyp 
Ref 
Expression 
1 

algcvgb.1 
⊢ 𝐹 : 𝑆 ⟶ 𝑆 
2 

algcvgb.2 
⊢ 𝐶 : 𝑆 ⟶ ℕ_{0} 
3 
2

ffvelrni 
⊢ ( 𝑋 ∈ 𝑆 → ( 𝐶 ‘ 𝑋 ) ∈ ℕ_{0} ) 
4 
1

ffvelrni 
⊢ ( 𝑋 ∈ 𝑆 → ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 ) 
5 
2

ffvelrni 
⊢ ( ( 𝐹 ‘ 𝑋 ) ∈ 𝑆 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℕ_{0} ) 
6 
4 5

syl 
⊢ ( 𝑋 ∈ 𝑆 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℕ_{0} ) 
7 

algcvgblem 
⊢ ( ( ( 𝐶 ‘ 𝑋 ) ∈ ℕ_{0} ∧ ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ∈ ℕ_{0} ) → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ↔ ( ( ( 𝐶 ‘ 𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ∧ ( ( 𝐶 ‘ 𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) = 0 ) ) ) ) 
8 
3 6 7

syl2anc 
⊢ ( 𝑋 ∈ 𝑆 → ( ( ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ↔ ( ( ( 𝐶 ‘ 𝑋 ) ≠ 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) < ( 𝐶 ‘ 𝑋 ) ) ∧ ( ( 𝐶 ‘ 𝑋 ) = 0 → ( 𝐶 ‘ ( 𝐹 ‘ 𝑋 ) ) = 0 ) ) ) ) 