Theorem tfrlem8

Description: Lemma for transfinite recursion. The domain of recs is an ordinal. (Contributed by NM, 14-Aug-1994) (Proof shortened by Alan Sare, 11-Mar-2008)

	Ref	Expression
Hypothesis	tfrlem.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Assertion	tfrlem8	|- Ord dom recs ( F )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2	1	tfrlem3	|- A = { g | E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) }
3	2	eqabri	|- ( g e. A <-> E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )
4		fndm	|- ( g Fn z -> dom g = z )
5	4	adantr	|- ( ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) -> dom g = z )
6	5	eleq1d	|- ( ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) -> ( dom g e. On <-> z e. On ) )
7	6	biimprcd	|- ( z e. On -> ( ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) -> dom g e. On ) )
8	7	rexlimiv	|- ( E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) -> dom g e. On )
9	3 8	sylbi	|- ( g e. A -> dom g e. On )
10		eleq1a	|- ( dom g e. On -> ( z = dom g -> z e. On ) )
11	9 10	syl	|- ( g e. A -> ( z = dom g -> z e. On ) )
12	11	rexlimiv	|- ( E. g e. A z = dom g -> z e. On )
13	12	abssi	|- { z | E. g e. A z = dom g } C_ On
14		ssorduni	|- ( { z | E. g e. A z = dom g } C_ On -> Ord U. { z | E. g e. A z = dom g } )
15	13 14	ax-mp	|- Ord U. { z | E. g e. A z = dom g }
16	1	recsfval	|- recs ( F ) = U. A
17	16	dmeqi	|- dom recs ( F ) = dom U. A
18		dmuni	|- dom U. A = U_ g e. A dom g
19		vex	|- g e. _V
20	19	dmex	|- dom g e. _V
21	20	dfiun2	|- U_ g e. A dom g = U. { z | E. g e. A z = dom g }
22	17 18 21	3eqtri	|- dom recs ( F ) = U. { z | E. g e. A z = dom g }
23		ordeq	|- ( dom recs ( F ) = U. { z | E. g e. A z = dom g } -> ( Ord dom recs ( F ) <-> Ord U. { z | E. g e. A z = dom g } ) )
24	22 23	ax-mp	|- ( Ord dom recs ( F ) <-> Ord U. { z | E. g e. A z = dom g } )
25	15 24	mpbir	|- Ord dom recs ( F )