Metamath Proof Explorer

Theorem frrlem2

Description: Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012)

Ref Expression
Hypothesis frrlem1.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y G f ↾ Pred R A y
Assertion frrlem2 ⊢ g ∈ B → Fun ⁡ g

Proof

Step Hyp Ref Expression
1 frrlem1.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = y G f ↾ Pred R A y
2 1 frrlem1 ⊢ B = g | ∃ z g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = w G g ↾ Pred R A w
3 2 eqabri ⊢ g ∈ B ↔ ∃ z g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = w G g ↾ Pred R A w
4 fnfun ⊢ g Fn z → Fun ⁡ g
5 4 3ad2ant1 ⊢ g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = w G g ↾ Pred R A w → Fun ⁡ g
6 5 exlimiv ⊢ ∃ z g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = w G g ↾ Pred R A w → Fun ⁡ g
7 3 6 sylbi ⊢ g ∈ B → Fun ⁡ g