# Metamath Proof Explorer

## Theorem tfrlem7

Description: Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994) (Revised by Mario Carneiro, 24-May-2019)

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

### Proof

Step Hyp Ref Expression
1 tfrlem.1 $⊢ A = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = F ⁡ f ↾ y$
2 1 tfrlem6 $⊢ Rel ⁡ recs ⁡ F$
3 1 recsfval $⊢ recs ⁡ F = ⋃ A$
4 3 eleq2i $⊢ x u ∈ recs ⁡ F ↔ x u ∈ ⋃ A$
5 eluni $⊢ x u ∈ ⋃ A ↔ ∃ g x u ∈ g ∧ g ∈ A$
6 4 5 bitri $⊢ x u ∈ recs ⁡ F ↔ ∃ g x u ∈ g ∧ g ∈ A$
7 3 eleq2i $⊢ x v ∈ recs ⁡ F ↔ x v ∈ ⋃ A$
8 eluni $⊢ x v ∈ ⋃ A ↔ ∃ h x v ∈ h ∧ h ∈ A$
9 7 8 bitri $⊢ x v ∈ recs ⁡ F ↔ ∃ h x v ∈ h ∧ h ∈ A$
10 6 9 anbi12i $⊢ x u ∈ recs ⁡ F ∧ x v ∈ recs ⁡ F ↔ ∃ g x u ∈ g ∧ g ∈ A ∧ ∃ h x v ∈ h ∧ h ∈ A$
11 exdistrv $⊢ ∃ g ∃ h x u ∈ g ∧ g ∈ A ∧ x v ∈ h ∧ h ∈ A ↔ ∃ g x u ∈ g ∧ g ∈ A ∧ ∃ h x v ∈ h ∧ h ∈ A$
12 10 11 bitr4i $⊢ x u ∈ recs ⁡ F ∧ x v ∈ recs ⁡ F ↔ ∃ g ∃ h x u ∈ g ∧ g ∈ A ∧ x v ∈ h ∧ h ∈ A$
13 df-br $⊢ x g u ↔ x u ∈ g$
14 df-br $⊢ x h v ↔ x v ∈ h$
15 13 14 anbi12i $⊢ x g u ∧ x h v ↔ x u ∈ g ∧ x v ∈ h$
16 1 tfrlem5 $⊢ g ∈ A ∧ h ∈ A → x g u ∧ x h v → u = v$
17 16 impcom $⊢ x g u ∧ x h v ∧ g ∈ A ∧ h ∈ A → u = v$
18 15 17 sylanbr $⊢ x u ∈ g ∧ x v ∈ h ∧ g ∈ A ∧ h ∈ A → u = v$
19 18 an4s $⊢ x u ∈ g ∧ g ∈ A ∧ x v ∈ h ∧ h ∈ A → u = v$
20 19 exlimivv $⊢ ∃ g ∃ h x u ∈ g ∧ g ∈ A ∧ x v ∈ h ∧ h ∈ A → u = v$
21 12 20 sylbi $⊢ x u ∈ recs ⁡ F ∧ x v ∈ recs ⁡ F → u = v$
22 21 ax-gen $⊢ ∀ v x u ∈ recs ⁡ F ∧ x v ∈ recs ⁡ F → u = v$
23 22 gen2 $⊢ ∀ x ∀ u ∀ v x u ∈ recs ⁡ F ∧ x v ∈ recs ⁡ F → u = v$
24 dffun4 $⊢ Fun ⁡ recs ⁡ F ↔ Rel ⁡ recs ⁡ F ∧ ∀ x ∀ u ∀ v x u ∈ recs ⁡ F ∧ x v ∈ recs ⁡ F → u = v$
25 2 23 24 mpbir2an $⊢ Fun ⁡ recs ⁡ F$