Metamath Proof Explorer

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 ∈ P → G ⁡ z ∈ P
Assertion findabrcl ⊢ C ∈ ω ∧ A ∈ P → x ∈ V ⟼ rec ⁡ G A ⁡ x ⁡ C ∈ P

Proof

Step Hyp Ref Expression
1 findabrcl.1 ⊢ z ∈ P → G ⁡ z ∈ P
2 elex ⊢ C ∈ ω → C ∈ V
3 fveq2 ⊢ x = C → rec ⁡ G A ⁡ x = rec ⁡ G A ⁡ C
4 eqid ⊢ x ∈ V ⟼ rec ⁡ G A ⁡ x = x ∈ V ⟼ rec ⁡ G A ⁡ x
5 fvex ⊢ rec ⁡ G A ⁡ C ∈ V
6 3 4 5 fvmpt ⊢ C ∈ V → x ∈ V ⟼ rec ⁡ G A ⁡ x ⁡ C = rec ⁡ G A ⁡ C
7 2 6 syl ⊢ C ∈ ω → x ∈ V ⟼ rec ⁡ G A ⁡ x ⁡ C = rec ⁡ G A ⁡ C
8 7 adantr ⊢ C ∈ ω ∧ A ∈ P → x ∈ V ⟼ rec ⁡ G A ⁡ x ⁡ C = rec ⁡ G A ⁡ C
9 1 findreccl ⊢ C ∈ ω → A ∈ P → rec ⁡ G A ⁡ C ∈ P
10 9 imp ⊢ C ∈ ω ∧ A ∈ P → rec ⁡ G A ⁡ C ∈ P
11 8 10 eqeltrd ⊢ C ∈ ω ∧ A ∈ P → x ∈ V ⟼ rec ⁡ G A ⁡ x ⁡ C ∈ P