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

Metamath Proof Explorer

Theorem recsfval

Description: Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015)

Ref Expression
Hypothesis tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
Assertion recsfval ⊢ recs ⁡ F = ⋃ A

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
2 dfrecs3 ⊢ recs ⁡ F = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
3 1 unieqi ⊢ ⋃ A = ⋃ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y
4 2 3 eqtr4i ⊢ recs ⁡ F = ⋃ A