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 ⁡ G A ⁡ C ∈ P

Proof

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