Metamath Proof Explorer

Theorem bnj60

Description: Well-founded recursion, part 1 of 3. The proof has been taken from Chapter 4 of Don Monk's notes on Set Theory. See http://euclid.colorado.edu/~monkd/setth.pdf . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj60.1 ⊢B=d|d⊆A∧∀x∈dpredxAR⊆d
bnj60.2 ⊢Y=xf↾predxAR
bnj60.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
bnj60.4 ⊢F=⋃C
Assertion bnj60 ⊢RFrSeA→FFnA

Proof

Step Hyp Ref Expression
1 bnj60.1 ⊢B=d|d⊆A∧∀x∈dpredxAR⊆d
2 bnj60.2 ⊢Y=xf↾predxAR
3 bnj60.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
4 bnj60.4 ⊢F=⋃C
5 1 2 3 bnj1497 ⊢∀g∈CFun⁡g
6 eqid ⊢dom⁡g∩dom⁡h=dom⁡g∩dom⁡h
7 1 2 3 6 bnj1311 ⊢RFrSeA∧g∈C∧h∈C→g↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h
8 7 3expia ⊢RFrSeA∧g∈C→h∈C→g↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h
9 8 ralrimiv ⊢RFrSeA∧g∈C→∀h∈Cg↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h
10 9 ralrimiva ⊢RFrSeA→∀g∈C∀h∈Cg↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h
11 biid ⊢∀g∈CFun⁡g↔∀g∈CFun⁡g
12 biid ⊢∀g∈CFun⁡g∧∀g∈C∀h∈Cg↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h↔∀g∈CFun⁡g∧∀g∈C∀h∈Cg↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h
13 11 6 12 bnj1383 ⊢∀g∈CFun⁡g∧∀g∈C∀h∈Cg↾dom⁡g∩dom⁡h=h↾dom⁡g∩dom⁡h→Fun⁡⋃C
14 5 10 13 sylancr ⊢RFrSeA→Fun⁡⋃C
15 4 funeqi ⊢Fun⁡F↔Fun⁡⋃C
16 14 15 sylibr ⊢RFrSeA→Fun⁡F
17 1 2 3 4 bnj1498 ⊢RFrSeA→dom⁡F=A
18 16 17 bnj1422 ⊢RFrSeA→FFnA