Theorem findfvcl

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

	Ref	Expression
Hypotheses	findfvcl.1	$$⊢\phi \to F\left(\varnothing \right)\in P$$
	findfvcl.2	$$⊢y\in \mathrm{\omega }\to \left(\phi \to \left(F\left(y\right)\in P\to F\left(\mathrm{suc}y\right)\in P\right)\right)$$
Assertion	findfvcl	$$⊢A\in \mathrm{\omega }\to \left(\phi \to F\left(A\right)\in P\right)$$

Proof

Step	Hyp	Ref	Expression
1		findfvcl.1	$$⊢\phi \to F\left(\varnothing \right)\in P$$
2		findfvcl.2	$$⊢y\in \mathrm{\omega }\to \left(\phi \to \left(F\left(y\right)\in P\to F\left(\mathrm{suc}y\right)\in P\right)\right)$$
3		fveleq	$$⊢x=\varnothing \to \left(\left(\phi \to F\left(x\right)\in P\right)\leftrightarrow \left(\phi \to F\left(\varnothing \right)\in P\right)\right)$$
4		fveleq	$$⊢x=y\to \left(\left(\phi \to F\left(x\right)\in P\right)\leftrightarrow \left(\phi \to F\left(y\right)\in P\right)\right)$$
5		fveleq	$$⊢x=\mathrm{suc}y\to \left(\left(\phi \to F\left(x\right)\in P\right)\leftrightarrow \left(\phi \to F\left(\mathrm{suc}y\right)\in P\right)\right)$$
6		fveleq	$$⊢x=A\to \left(\left(\phi \to F\left(x\right)\in P\right)\leftrightarrow \left(\phi \to F\left(A\right)\in P\right)\right)$$
7	2	a2d	$$⊢y\in \mathrm{\omega }\to \left(\left(\phi \to F\left(y\right)\in P\right)\to \left(\phi \to F\left(\mathrm{suc}y\right)\in P\right)\right)$$
8	3 4 5 6 1 7	finds	$$⊢A\in \mathrm{\omega }\to \left(\phi \to F\left(A\right)\in P\right)$$