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