This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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