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 C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
	bnj60.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
	bnj60.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
	bnj60.4	|- F = U. C
Assertion	bnj60	|- ( R _FrSe A -> F Fn A )

Proof

Step	Hyp	Ref	Expression
1		bnj60.1	|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2		bnj60.2	|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3		bnj60.3	|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4		bnj60.4	|- F = U. C
5	1 2 3	bnj1497	|- A. g e. C Fun g
6		eqid	|- ( dom g i^i dom h ) = ( dom g i^i dom h )
7	1 2 3 6	bnj1311	|- ( ( R _FrSe A /\ g e. C /\ h e. C ) -> ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) )
8	7	3expia	|- ( ( R _FrSe A /\ g e. C ) -> ( h e. C -> ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) ) )
9	8	ralrimiv	|- ( ( R _FrSe A /\ g e. C ) -> A. h e. C ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) )
10	9	ralrimiva	|- ( R _FrSe A -> A. g e. C A. h e. C ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) )
11		biid	|- ( A. g e. C Fun g <-> A. g e. C Fun g )
12		biid	|- ( ( A. g e. C Fun g /\ A. g e. C A. h e. C ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) ) <-> ( A. g e. C Fun g /\ A. g e. C A. h e. C ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) ) )
13	11 6 12	bnj1383	|- ( ( A. g e. C Fun g /\ A. g e. C A. h e. C ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) ) -> Fun U. C )
14	5 10 13	sylancr	|- ( R _FrSe A -> Fun U. C )
15	4	funeqi	|- ( Fun F <-> Fun U. C )
16	14 15	sylibr	|- ( R _FrSe A -> Fun F )
17	1 2 3 4	bnj1498	|- ( R _FrSe A -> dom F = A )
18	16 17	bnj1422	|- ( R _FrSe A -> F Fn A )