Theorem findfvcl

Description: Please add description here. (Contributed by Jeff Hoffman, 12-Feb-2008)

	Ref	Expression
Hypotheses	findfvcl.1	⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) ∈ 𝑃 )
	findfvcl.2	⊢ ( 𝑦 ∈ ω → ( 𝜑 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑃 → ( 𝐹 ‘ suc 𝑦 ) ∈ 𝑃 ) ) )
Assertion	findfvcl	⊢ ( 𝐴 ∈ ω → ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		findfvcl.1	⊢ ( 𝜑 → ( 𝐹 ‘ ∅ ) ∈ 𝑃 )
2		findfvcl.2	⊢ ( 𝑦 ∈ ω → ( 𝜑 → ( ( 𝐹 ‘ 𝑦 ) ∈ 𝑃 → ( 𝐹 ‘ suc 𝑦 ) ∈ 𝑃 ) ) )
3		fveleq	⊢ ( 𝑥 = ∅ → ( ( 𝜑 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑃 ) ↔ ( 𝜑 → ( 𝐹 ‘ ∅ ) ∈ 𝑃 ) ) )
4		fveleq	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑃 ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝑦 ) ∈ 𝑃 ) ) )
5		fveleq	⊢ ( 𝑥 = suc 𝑦 → ( ( 𝜑 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑃 ) ↔ ( 𝜑 → ( 𝐹 ‘ suc 𝑦 ) ∈ 𝑃 ) ) )
6		fveleq	⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → ( 𝐹 ‘ 𝑥 ) ∈ 𝑃 ) ↔ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑃 ) ) )
7	2	a2d	⊢ ( 𝑦 ∈ ω → ( ( 𝜑 → ( 𝐹 ‘ 𝑦 ) ∈ 𝑃 ) → ( 𝜑 → ( 𝐹 ‘ suc 𝑦 ) ∈ 𝑃 ) ) )
8	3 4 5 6 1 7	finds	⊢ ( 𝐴 ∈ ω → ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ 𝑃 ) )