Theorem findabrcl

Description: Please add description here. (Contributed by Jeff Hoffman, 16-Feb-2008) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypothesis	findabrcl.1	|- ( z e. P -> ( G ` z ) e. P )
Assertion	findabrcl	|- ( ( C e. _om /\ A e. P ) -> ( ( x e. _V |-> ( rec ( G , A ) ` x ) ) ` C ) e. P )

Proof

Step	Hyp	Ref	Expression
1		findabrcl.1	|- ( z e. P -> ( G ` z ) e. P )
2		elex	|- ( C e. _om -> C e. _V )
3		fveq2	|- ( x = C -> ( rec ( G , A ) ` x ) = ( rec ( G , A ) ` C ) )
4		eqid	|- ( x e. _V |-> ( rec ( G , A ) ` x ) ) = ( x e. _V |-> ( rec ( G , A ) ` x ) )
5		fvex	|- ( rec ( G , A ) ` C ) e. _V
6	3 4 5	fvmpt	|- ( C e. _V -> ( ( x e. _V |-> ( rec ( G , A ) ` x ) ) ` C ) = ( rec ( G , A ) ` C ) )
7	2 6	syl	|- ( C e. _om -> ( ( x e. _V |-> ( rec ( G , A ) ` x ) ) ` C ) = ( rec ( G , A ) ` C ) )
8	7	adantr	|- ( ( C e. _om /\ A e. P ) -> ( ( x e. _V |-> ( rec ( G , A ) ` x ) ) ` C ) = ( rec ( G , A ) ` C ) )
9	1	findreccl	|- ( C e. _om -> ( A e. P -> ( rec ( G , A ) ` C ) e. P ) )
10	9	imp	|- ( ( C e. _om /\ A e. P ) -> ( rec ( G , A ) ` C ) e. P )
11	8 10	eqeltrd	|- ( ( C e. _om /\ A e. P ) -> ( ( x e. _V |-> ( rec ( G , A ) ` x ) ) ` C ) e. P )