Theorem findreccl

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

	Ref	Expression
Hypothesis	findreccl.1	⊢ ( 𝑧 ∈ 𝑃 → ( 𝐺 ‘ 𝑧 ) ∈ 𝑃 )
Assertion	findreccl	⊢ ( 𝐶 ∈ ω → ( 𝐴 ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) ∈ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		findreccl.1	⊢ ( 𝑧 ∈ 𝑃 → ( 𝐺 ‘ 𝑧 ) ∈ 𝑃 )
2		rdg0g	⊢ ( 𝐴 ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ ∅ ) = 𝐴 )
3		eleq1a	⊢ ( 𝐴 ∈ 𝑃 → ( ( rec ( 𝐺 , 𝐴 ) ‘ ∅ ) = 𝐴 → ( rec ( 𝐺 , 𝐴 ) ‘ ∅ ) ∈ 𝑃 ) )
4	2 3	mpd	⊢ ( 𝐴 ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ ∅ ) ∈ 𝑃 )
5		nnon	⊢ ( 𝑦 ∈ ω → 𝑦 ∈ On )
6		fveq2	⊢ ( 𝑧 = ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ) )
7	6	eleq1d	⊢ ( 𝑧 = ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ 𝑃 ↔ ( 𝐺 ‘ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ) ∈ 𝑃 ) )
8	7 1	vtoclga	⊢ ( ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ∈ 𝑃 → ( 𝐺 ‘ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ) ∈ 𝑃 )
9		rdgsuc	⊢ ( 𝑦 ∈ On → ( rec ( 𝐺 , 𝐴 ) ‘ suc 𝑦 ) = ( 𝐺 ‘ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ) )
10	9	eleq1d	⊢ ( 𝑦 ∈ On → ( ( rec ( 𝐺 , 𝐴 ) ‘ suc 𝑦 ) ∈ 𝑃 ↔ ( 𝐺 ‘ ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ) ∈ 𝑃 ) )
11	8 10	imbitrrid	⊢ ( 𝑦 ∈ On → ( ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ suc 𝑦 ) ∈ 𝑃 ) )
12	5 11	syl	⊢ ( 𝑦 ∈ ω → ( ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ suc 𝑦 ) ∈ 𝑃 ) )
13	12	a1d	⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ 𝑃 → ( ( rec ( 𝐺 , 𝐴 ) ‘ 𝑦 ) ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ suc 𝑦 ) ∈ 𝑃 ) ) )
14	4 13	findfvcl	⊢ ( 𝐶 ∈ ω → ( 𝐴 ∈ 𝑃 → ( rec ( 𝐺 , 𝐴 ) ‘ 𝐶 ) ∈ 𝑃 ) )