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	⊢ ( 𝑧 ∈ 𝑃 → ( 𝐺 ‘ 𝑧 ) ∈ 𝑃 )
Assertion	findabrcl	⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃 ) → ( ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) ) ‘ 𝐶 ) ∈ 𝑃 )

Proof

Step	Hyp	Ref	Expression
1		findabrcl.1	⊢ ( 𝑧 ∈ 𝑃 → ( 𝐺 ‘ 𝑧 ) ∈ 𝑃 )
2		elex	⊢ ( 𝐶 ∈ ω → 𝐶 ∈ V )
3		fveq2	⊢ ( 𝑥 = 𝐶 → ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) = ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) )
4		eqid	⊢ ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) ) = ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) )
5		fvex	⊢ ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝐶 ∈ V → ( ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) ) ‘ 𝐶 ) = ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) )
7	2 6	syl	⊢ ( 𝐶 ∈ ω → ( ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) ) ‘ 𝐶 ) = ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) )
8	7	adantr	⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃 ) → ( ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) ) ‘ 𝐶 ) = ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) )
9	1	findreccl	⊢ ( 𝐶 ∈ ω → ( 𝐴 ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) ∈ 𝑃 ) )
10	9	imp	⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃 ) → ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) ∈ 𝑃 )
11	8 10	eqeltrd	⊢ ( ( 𝐶 ∈ ω ∧ 𝐴 ∈ 𝑃 ) → ( ( 𝑥 ∈ V ↦ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑥 ) ) ‘ 𝐶 ) ∈ 𝑃 )