Theorem tfrlem10

Description: Lemma for transfinite recursion. We define class C by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On . Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem14 , thus showing the domain of recs does in fact equal On . Here we show (under the false assumption) that C is a function extending the domain of recs ( F ) by one. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	tfrlem.1	|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
	tfrlem.3	|- C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
Assertion	tfrlem10	|- ( dom recs ( F ) e. On -> C Fn suc 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		tfrlem.3	|- C = ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
3		fvex	|- ( F ` recs ( F ) ) e. _V
4		funsng	|- ( ( dom recs ( F ) e. On /\ ( F ` recs ( F ) ) e. _V ) -> Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
5	3 4	mpan2	|- ( dom recs ( F ) e. On -> Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
6	1	tfrlem7	|- Fun recs ( F )
7	5 6	jctil	|- ( dom recs ( F ) e. On -> ( Fun recs ( F ) /\ Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
8	3	dmsnop	|- dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } = { dom recs ( F ) }
9	8	ineq2i	|- ( dom recs ( F ) i^i dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( dom recs ( F ) i^i { dom recs ( F ) } )
10	1	tfrlem8	|- Ord dom recs ( F )
11		orddisj	|- ( Ord dom recs ( F ) -> ( dom recs ( F ) i^i { dom recs ( F ) } ) = (/) )
12	10 11	ax-mp	|- ( dom recs ( F ) i^i { dom recs ( F ) } ) = (/)
13	9 12	eqtri	|- ( dom recs ( F ) i^i dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = (/)
14		funun	|- ( ( ( Fun recs ( F ) /\ Fun { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) /\ ( dom recs ( F ) i^i dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = (/) ) -> Fun ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
15	7 13 14	sylancl	|- ( dom recs ( F ) e. On -> Fun ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
16	8	uneq2i	|- ( dom recs ( F ) u. dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( dom recs ( F ) u. { dom recs ( F ) } )
17		dmun	|- dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = ( dom recs ( F ) u. dom { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
18		df-suc	|- suc dom recs ( F ) = ( dom recs ( F ) u. { dom recs ( F ) } )
19	16 17 18	3eqtr4i	|- dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = suc dom recs ( F )
20		df-fn	|- ( ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) <-> ( Fun ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) /\ dom ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) = suc dom recs ( F ) ) )
21	15 19 20	sylanblrc	|- ( dom recs ( F ) e. On -> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) )
22	2	fneq1i	|- ( C Fn suc dom recs ( F ) <-> ( recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) Fn suc dom recs ( F ) )
23	21 22	sylibr	|- ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )