Theorem findfvcl

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

	Ref	Expression
Hypotheses	findfvcl.1	|- ( ph -> ( F ` (/) ) e. P )
	findfvcl.2	|- ( y e. _om -> ( ph -> ( ( F ` y ) e. P -> ( F ` suc y ) e. P ) ) )
Assertion	findfvcl	|- ( A e. _om -> ( ph -> ( F ` A ) e. P ) )

Proof

Step	Hyp	Ref	Expression
1		findfvcl.1	|- ( ph -> ( F ` (/) ) e. P )
2		findfvcl.2	|- ( y e. _om -> ( ph -> ( ( F ` y ) e. P -> ( F ` suc y ) e. P ) ) )
3		fveleq	|- ( x = (/) -> ( ( ph -> ( F ` x ) e. P ) <-> ( ph -> ( F ` (/) ) e. P ) ) )
4		fveleq	|- ( x = y -> ( ( ph -> ( F ` x ) e. P ) <-> ( ph -> ( F ` y ) e. P ) ) )
5		fveleq	|- ( x = suc y -> ( ( ph -> ( F ` x ) e. P ) <-> ( ph -> ( F ` suc y ) e. P ) ) )
6		fveleq	|- ( x = A -> ( ( ph -> ( F ` x ) e. P ) <-> ( ph -> ( F ` A ) e. P ) ) )
7	2	a2d	|- ( y e. _om -> ( ( ph -> ( F ` y ) e. P ) -> ( ph -> ( F ` suc y ) e. P ) ) )
8	3 4 5 6 1 7	finds	|- ( A e. _om -> ( ph -> ( F ` A ) e. P ) )