Metamath Proof Explorer

Theorem wfrlem3a

Description: Lemma for well-ordered recursion. Show membership in the class of acceptable functions. (Contributed by Scott Fenton, 31-Jul-2020)

Ref Expression
Hypotheses wfrlem1.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ Pred R A y
wfrlem3a.2 ⊢ G ∈ V
Assertion wfrlem3a ⊢ G ∈ B ↔ ∃ z G Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z G ⁡ w = F ⁡ G ↾ Pred R A w

Proof

Step Hyp Ref Expression
1 wfrlem1.1 ⊢ B = f | ∃ x f Fn x ∧ x ⊆ A ∧ ∀ y ∈ x Pred R A y ⊆ x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ Pred R A y
2 wfrlem3a.2 ⊢ G ∈ V
3 fneq1 ⊢ g = G → g Fn z ↔ G Fn z
4 fveq1 ⊢ g = G → g ⁡ w = G ⁡ w
5 reseq1 ⊢ g = G → g ↾ Pred R A w = G ↾ Pred R A w
6 5 fveq2d ⊢ g = G → F ⁡ g ↾ Pred R A w = F ⁡ G ↾ Pred R A w
7 4 6 eqeq12d ⊢ g = G → g ⁡ w = F ⁡ g ↾ Pred R A w ↔ G ⁡ w = F ⁡ G ↾ Pred R A w
8 7 ralbidv ⊢ g = G → ∀ w ∈ z g ⁡ w = F ⁡ g ↾ Pred R A w ↔ ∀ w ∈ z G ⁡ w = F ⁡ G ↾ Pred R A w
9 3 8 3anbi13d ⊢ g = G → g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ Pred R A w ↔ G Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z G ⁡ w = F ⁡ G ↾ Pred R A w
10 9 exbidv ⊢ g = G → ∃ z g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ Pred R A w ↔ ∃ z G Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z G ⁡ w = F ⁡ G ↾ Pred R A w
11 1 wfrlem1 ⊢ B = g | ∃ z g Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ Pred R A w
12 2 10 11 elab2 ⊢ G ∈ B ↔ ∃ z G Fn z ∧ z ⊆ A ∧ ∀ w ∈ z Pred R A w ⊆ z ∧ ∀ w ∈ z G ⁡ w = F ⁡ G ↾ Pred R A w