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∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
Assertion tfrlem7 ⊢Fun⁡recs⁡F

Proof

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