Theorem bnj60 29883

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.)

Hypotheses

Ref	Expression
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

Ref	Expression
bnj60	|- ( R FrSe A -> F Fn A )

Distinct variable groups:   A, d, f, x   B, f   G, d, f, x   R, d, f, x

Allowed substitution hints:   B( x, d)   C( x, f, d)   F( x, f, d)   Y( x, f, d)

Proof of Theorem bnj60

Dummy variables g h are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bnj60.1	. . . . 5 |- B = { d | ( d C_ A /\ A. x e. d pred ( x , A , R ) C_ d ) }
2		bnj60.2	. . . . 5 |- Y = <. x , ( f |` pred ( x , A , R ) ) >.
3		bnj60.3	. . . . 5 |- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4	1, 2, 3	bnj1497 29881	. . . 4 |- A. g e. C Fun g
5		eqid 2453	. . . . . . . 8 |- ( dom g i^i dom h ) = ( dom g i^i dom h )
6	1, 2, 3, 5	bnj1311 29845	. . . . . . 7 |- ( ( R FrSe A /\ g e. C /\ h e. C ) -> ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) )
7	6	3expia 1211	. . . . . 6 |- ( ( 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	ralrimiv 2802	. . . . 5 |- ( ( R FrSe A /\ g e. C ) -> A. h e. C ( g |` ( dom g i^i dom h ) ) = ( h |` ( dom g i^i dom h ) ) )
9	8	ralrimiva 2804	. . . 4 |- ( 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 ) ) )
10		biid 240	. . . . 5 |- ( A. g e. C Fun g <-> A. g e. C Fun g )
11		biid 240	. . . . 5 |- ( ( 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 ) ) ) )
12	10, 5, 11	bnj1383 29655	. . . 4 |- ( ( 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 )
13	4, 9, 12	sylancr 670	. . 3 |- ( R FrSe A -> Fun U. C )
14		bnj60.4	. . . 4 |- F = U. C
15	14	funeqi 5605	. . 3 |- ( Fun F <-> Fun U. C )
16	13, 15	sylibr 216	. 2 |- ( R FrSe A -> Fun F )
17	1, 2, 3, 14	bnj1498 29882	. 2 |- ( R FrSe A -> dom F = A )
18	16, 17	bnj1422 29661	1 |- ( R FrSe A -> F Fn A )

Syntax hints:   -> wi 4   /\ wa 371   = wceq 1446   e. wcel 1889   {cab 2439   A.wral 2739   E.wrex 2740   i^i cin 3405   C_ wss 3406   <.cop 3976   U.cuni 4201   dom cdm 4837   |` cres 4839   Fun wfun 5579   Fn wfn 5580   ` cfv 5585   predc-bnj14 29505   FrSe w-bnj15 29509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-rep 4518  ax-sep 4528  ax-nul 4537  ax-pow 4584  ax-pr 4642  ax-un 6588  ax-reg 8112  ax-inf2 8151

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 987  df-3an 988  df-tru 1449  df-fal 1452  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3734  df-if 3884  df-pw 3955  df-sn 3971  df-pr 3973  df-tp 3975  df-op 3977  df-uni 4202  df-iun 4283  df-br 4406  df-opab 4465  df-mpt 4466  df-tr 4501  df-eprel 4748  df-id 4752  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-ord 5429  df-on 5430  df-lim 5431  df-suc 5432  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593  df-om 6698  df-1o 7187  df-bnj17 29504  df-bnj14 29506  df-bnj13 29508  df-bnj15 29510  df-bnj18 29512  df-bnj19 29514

This theorem is referenced by:  bnj1501  29888  bnj1523  29892