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 )

Metamath Proof Explorer

Theorem tfrlem8

Proof