Metamath Proof Explorer

Theorem findreccl

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

Ref Expression
Hypothesis findreccl.1 ⊢z∈P→G⁡z∈P
Assertion findreccl ⊢C∈ω→A∈P→rec⁡GA⁡C∈P

Proof

Step Hyp Ref Expression
1 findreccl.1 ⊢z∈P→G⁡z∈P
2 rdg0g ⊢A∈P→rec⁡GA⁡∅=A
3 eleq1a ⊢A∈P→rec⁡GA⁡∅=A→rec⁡GA⁡∅∈P
4 2 3 mpd ⊢A∈P→rec⁡GA⁡∅∈P
5 nnon ⊢y∈ω→y∈On
6 fveq2 ⊢z=rec⁡GA⁡y→G⁡z=G⁡rec⁡GA⁡y
7 6 eleq1d ⊢z=rec⁡GA⁡y→G⁡z∈P↔G⁡rec⁡GA⁡y∈P
8 7 1 vtoclga ⊢rec⁡GA⁡y∈P→G⁡rec⁡GA⁡y∈P
9 rdgsuc ⊢y∈On→rec⁡GA⁡suc⁡y=G⁡rec⁡GA⁡y
10 9 eleq1d ⊢y∈On→rec⁡GA⁡suc⁡y∈P↔G⁡rec⁡GA⁡y∈P
11 8 10 imbitrrid ⊢y∈On→rec⁡GA⁡y∈P→rec⁡GA⁡suc⁡y∈P
12 5 11 syl ⊢y∈ω→rec⁡GA⁡y∈P→rec⁡GA⁡suc⁡y∈P
13 12 a1d ⊢y∈ω→A∈P→rec⁡GA⁡y∈P→rec⁡GA⁡suc⁡y∈P
14 4 13 findfvcl ⊢C∈ω→A∈P→rec⁡GA⁡C∈P