Metamath Proof Explorer

Theorem frrlem3

Description: Lemma for well-founded recursion. An acceptable function's domain is a subset of A . (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 frrlem3 ⊢ g ∈ B → dom ⁡ g ⊆ A

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 abeq2i ⊢ 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 fndm ⊢ g Fn z → dom ⁡ g = z
5 4 sseq1d ⊢ g Fn z → dom ⁡ g ⊆ A ↔ z ⊆ A
6 5 biimpar ⊢ g Fn z ∧ z ⊆ A → dom ⁡ g ⊆ A
7 6 adantrr ⊢ g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z → dom ⁡ g ⊆ A
8 7 3adant3 ⊢ g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = w G g ↾ Pred R A w → dom ⁡ g ⊆ A
9 8 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 → dom ⁡ g ⊆ A
10 3 9 sylbi ⊢ g ∈ B → dom ⁡ g ⊆ A