Theorem tfrlem11 7106

Description: Lemma for transfinite recursion. Compute the value of C. (Contributed by NM, 18-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.)

Hypotheses

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

Ref	Expression
tfrlem11	|- ( dom recs ( F ) e. On -> ( B e. suc dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )

Distinct variable groups:   x, f, y, B   C, f, x, y   f, F, x, y

Allowed substitution hints:   A( x, y, f)

Proof of Theorem tfrlem11

Step	Hyp	Ref	Expression
1		elsuci 5489	. 2 |- ( B e. suc dom recs ( F ) -> ( B e. dom recs ( F ) \/ B = dom recs ( F ) ) )
2		tfrlem.1	. . . . . . . . 9 |- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
3		tfrlem.3	. . . . . . . . 9 |- C = (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
4	2, 3	tfrlem10 7105	. . . . . . . 8 |- ( dom recs ( F ) e. On -> C Fn suc dom recs ( F ) )
5		fnfun 5673	. . . . . . . 8 |- ( C Fn suc dom recs ( F ) -> Fun C )
6	4, 5	syl 17	. . . . . . 7 |- ( dom recs ( F ) e. On -> Fun C )
7		ssun1 3597	. . . . . . . . 9 |- recs ( F ) C_ (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
8	7, 3	sseqtr4i 3465	. . . . . . . 8 |- recs ( F ) C_ C
9	2	tfrlem9 7103	. . . . . . . . 9 |- ( B e. dom recs ( F ) -> (recs ( F ) ` B ) = ( F ` (recs ( F ) |` B ) ) )
10		funssfv 5880	. . . . . . . . . . . 12 |- ( ( Fun C /\ recs ( F ) C_ C /\ B e. dom recs ( F ) ) -> ( C ` B ) = (recs ( F ) ` B ) )
11	10	3expa 1208	. . . . . . . . . . 11 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ B e. dom recs ( F ) ) -> ( C ` B ) = (recs ( F ) ` B ) )
12	11	adantrl 722	. . . . . . . . . 10 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( C ` B ) = (recs ( F ) ` B ) )
13		onelss 5465	. . . . . . . . . . . 12 |- ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> B C_ dom recs ( F ) ) )
14	13	imp 431	. . . . . . . . . . 11 |- ( ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) -> B C_ dom recs ( F ) )
15		fun2ssres 5623	. . . . . . . . . . . . 13 |- ( ( Fun C /\ recs ( F ) C_ C /\ B C_ dom recs ( F ) ) -> ( C |` B ) = (recs ( F ) |` B ) )
16	15	3expa 1208	. . . . . . . . . . . 12 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ B C_ dom recs ( F ) ) -> ( C |` B ) = (recs ( F ) |` B ) )
17	16	fveq2d 5869	. . . . . . . . . . 11 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ B C_ dom recs ( F ) ) -> ( F ` ( C |` B ) ) = ( F ` (recs ( F ) |` B ) ) )
18	14, 17	sylan2 477	. . . . . . . . . 10 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( F ` ( C |` B ) ) = ( F ` (recs ( F ) |` B ) ) )
19	12, 18	eqeq12d 2466	. . . . . . . . 9 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( ( C ` B ) = ( F ` ( C |` B ) ) <-> (recs ( F ) ` B ) = ( F ` (recs ( F ) |` B ) ) ) )
20	9, 19	syl5ibr 225	. . . . . . . 8 |- ( ( ( Fun C /\ recs ( F ) C_ C ) /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
21	8, 20	mpanl2 687	. . . . . . 7 |- ( ( Fun C /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
22	6, 21	sylan 474	. . . . . 6 |- ( ( dom recs ( F ) e. On /\ ( dom recs ( F ) e. On /\ B e. dom recs ( F ) ) ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
23	22	exp32 610	. . . . 5 |- ( dom recs ( F ) e. On -> ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) ) ) )
24	23	pm2.43i 49	. . . 4 |- ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) ) )
25	24	pm2.43d 50	. . 3 |- ( dom recs ( F ) e. On -> ( B e. dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
26		opex 4664	. . . . . . . . 9 |- <. B , ( F ` ( C |` B ) ) >. e. _V
27	26	snid 3996	. . . . . . . 8 |- <. B , ( F ` ( C |` B ) ) >. e. { <. B , ( F ` ( C |` B ) ) >. }
28		opeq1 4166	. . . . . . . . . . 11 |- ( B = dom recs ( F ) -> <. B , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` ( C |` B ) ) >. )
29	28	adantl 468	. . . . . . . . . 10 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` ( C |` B ) ) >. )
30		eqimss 3484	. . . . . . . . . . . . . 14 |- ( B = dom recs ( F ) -> B C_ dom recs ( F ) )
31	8, 15	mp3an2 1352	. . . . . . . . . . . . . 14 |- ( ( Fun C /\ B C_ dom recs ( F ) ) -> ( C |` B ) = (recs ( F ) |` B ) )
32	6, 30, 31	syl2an 480	. . . . . . . . . . . . 13 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( C |` B ) = (recs ( F ) |` B ) )
33		reseq2 5100	. . . . . . . . . . . . . . 15 |- ( B = dom recs ( F ) -> (recs ( F ) |` B ) = (recs ( F ) |` dom recs ( F ) ) )
34	2	tfrlem6 7100	. . . . . . . . . . . . . . . 16 |- Rel recs ( F )
35		resdm 5146	. . . . . . . . . . . . . . . 16 |- ( Rel recs ( F ) -> (recs ( F ) |` dom recs ( F ) ) = recs ( F ) )
36	34, 35	ax-mp 5	. . . . . . . . . . . . . . 15 |- (recs ( F ) |` dom recs ( F ) ) = recs ( F )
37	33, 36	syl6eq 2501	. . . . . . . . . . . . . 14 |- ( B = dom recs ( F ) -> (recs ( F ) |` B ) = recs ( F ) )
38	37	adantl 468	. . . . . . . . . . . . 13 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> (recs ( F ) |` B ) = recs ( F ) )
39	32, 38	eqtrd 2485	. . . . . . . . . . . 12 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( C |` B ) = recs ( F ) )
40	39	fveq2d 5869	. . . . . . . . . . 11 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( F ` ( C |` B ) ) = ( F ` recs ( F ) ) )
41	40	opeq2d 4173	. . . . . . . . . 10 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. dom recs ( F ) , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` recs ( F ) ) >. )
42	29, 41	eqtrd 2485	. . . . . . . . 9 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. = <. dom recs ( F ) , ( F ` recs ( F ) ) >. )
43	42	sneqd 3980	. . . . . . . 8 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> { <. B , ( F ` ( C |` B ) ) >. } = { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
44	27, 43	syl5eleq 2535	. . . . . . 7 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. e. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } )
45		elun2 3602	. . . . . . 7 |- ( <. B , ( F ` ( C |` B ) ) >. e. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } -> <. B , ( F ` ( C |` B ) ) >. e. (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
46	44, 45	syl 17	. . . . . 6 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. e. (recs ( F ) u. { <. dom recs ( F ) , ( F ` recs ( F ) ) >. } ) )
47	46, 3	syl6eleqr 2540	. . . . 5 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> <. B , ( F ` ( C |` B ) ) >. e. C )
48	4	adantr 467	. . . . . 6 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> C Fn suc dom recs ( F ) )
49		simpr 463	. . . . . . 7 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> B = dom recs ( F ) )
50		sucidg 5501	. . . . . . . 8 |- ( dom recs ( F ) e. On -> dom recs ( F ) e. suc dom recs ( F ) )
51	50	adantr 467	. . . . . . 7 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> dom recs ( F ) e. suc dom recs ( F ) )
52	49, 51	eqeltrd 2529	. . . . . 6 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> B e. suc dom recs ( F ) )
53		fnopfvb 5906	. . . . . 6 |- ( ( C Fn suc dom recs ( F ) /\ B e. suc dom recs ( F ) ) -> ( ( C ` B ) = ( F ` ( C |` B ) ) <-> <. B , ( F ` ( C |` B ) ) >. e. C ) )
54	48, 52, 53	syl2anc 667	. . . . 5 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( ( C ` B ) = ( F ` ( C |` B ) ) <-> <. B , ( F ` ( C |` B ) ) >. e. C ) )
55	47, 54	mpbird 236	. . . 4 |- ( ( dom recs ( F ) e. On /\ B = dom recs ( F ) ) -> ( C ` B ) = ( F ` ( C |` B ) ) )
56	55	ex 436	. . 3 |- ( dom recs ( F ) e. On -> ( B = dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
57	25, 56	jaod 382	. 2 |- ( dom recs ( F ) e. On -> ( ( B e. dom recs ( F ) \/ B = dom recs ( F ) ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )
58	1, 57	syl5 33	1 |- ( dom recs ( F ) e. On -> ( B e. suc dom recs ( F ) -> ( C ` B ) = ( F ` ( C |` B ) ) ) )

Syntax hints:   -> wi 4   <-> wb 188   \/ wo 370   /\ wa 371   = wceq 1444   e. wcel 1887   {cab 2437   A.wral 2737   E.wrex 2738   u. cun 3402   C_ wss 3404   {csn 3968   <.cop 3974   dom cdm 4834   |` cres 4836   Rel wrel 4839   Oncon0 5423   suc csuc 5425   Fun wfun 5576   Fn wfn 5577   ` cfv 5582  recscrecs 7089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-fv 5590  df-wrecs 7028  df-recs 7090

This theorem is referenced by:  tfrlem12  7107