This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tfrlem3

Description: Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995)

Ref Expression
Hypothesis tfrlem3.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
Assertion tfrlem3 ⊢ A = g | ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w

Proof

Step Hyp Ref Expression
1 tfrlem3.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
2 vex ⊢ g ∈ V
3 1 2 tfrlem3a ⊢ g ∈ A ↔ ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w
4 3 eqabi ⊢ A = g | ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = F ⁡ g ↾ w