Theorem tfrlem7 5933

Description: Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)

Hypothesis

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

Assertion

Ref	Expression
tfrlem7	|- Fun recs ( F )

Distinct variable group:   x, f, y, F

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

Proof of Theorem tfrlem7

Dummy variables g h u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfrlem.1	. . 3 |- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
2	1	tfrlem6 5932	. 2 |- Rel recs ( F )
3	1	recsfval 5931	. . . . . . . . 9 |- recs ( F ) = U. A
4	3	eleq2i 2104	. . . . . . . 8 |- ( <. x , u >. e. recs ( F ) <-> <. x , u >. e. U. A )
5		eluni 3583	. . . . . . . 8 |- ( <. x , u >. e. U. A <-> E. g ( <. x , u >. e. g /\ g e. A ) )
6	4, 5	bitri 173	. . . . . . 7 |- ( <. x , u >. e. recs ( F ) <-> E. g ( <. x , u >. e. g /\ g e. A ) )
7	3	eleq2i 2104	. . . . . . . 8 |- ( <. x , v >. e. recs ( F ) <-> <. x , v >. e. U. A )
8		eluni 3583	. . . . . . . 8 |- ( <. x , v >. e. U. A <-> E. h ( <. x , v >. e. h /\ h e. A ) )
9	7, 8	bitri 173	. . . . . . 7 |- ( <. x , v >. e. recs ( F ) <-> E. h ( <. x , v >. e. h /\ h e. A ) )
10	6, 9	anbi12i 433	. . . . . 6 |- ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) <-> ( E. g ( <. x , u >. e. g /\ g e. A ) /\ E. h ( <. x , v >. e. h /\ h e. A ) ) )
11		eeanv 1807	. . . . . 6 |- ( E. g E. h ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) <-> ( E. g ( <. x , u >. e. g /\ g e. A ) /\ E. h ( <. x , v >. e. h /\ h e. A ) ) )
12	10, 11	bitr4i 176	. . . . 5 |- ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) <-> E. g E. h ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) )
13		df-br 3765	. . . . . . . . 9 |- ( x g u <-> <. x , u >. e. g )
14		df-br 3765	. . . . . . . . 9 |- ( x h v <-> <. x , v >. e. h )
15	13, 14	anbi12i 433	. . . . . . . 8 |- ( ( x g u /\ x h v ) <-> ( <. x , u >. e. g /\ <. x , v >. e. h ) )
16	1	tfrlem5 5930	. . . . . . . . 9 |- ( ( g e. A /\ h e. A ) -> ( ( x g u /\ x h v ) -> u = v ) )
17	16	impcom 116	. . . . . . . 8 |- ( ( ( x g u /\ x h v ) /\ ( g e. A /\ h e. A ) ) -> u = v )
18	15, 17	sylanbr 269	. . . . . . 7 |- ( ( ( <. x , u >. e. g /\ <. x , v >. e. h ) /\ ( g e. A /\ h e. A ) ) -> u = v )
19	18	an4s 522	. . . . . 6 |- ( ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) -> u = v )
20	19	exlimivv 1776	. . . . 5 |- ( E. g E. h ( ( <. x , u >. e. g /\ g e. A ) /\ ( <. x , v >. e. h /\ h e. A ) ) -> u = v )
21	12, 20	sylbi 114	. . . 4 |- ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v )
22	21	ax-gen 1338	. . 3 |- A. v ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v )
23	22	gen2 1339	. 2 |- A. x A. u A. v ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v )
24		dffun4 4913	. 2 |- ( Fun recs ( F ) <-> ( Rel recs ( F ) /\ A. x A. u A. v ( ( <. x , u >. e. recs ( F ) /\ <. x , v >. e. recs ( F ) ) -> u = v ) ) )
25	2, 23, 24	mpbir2an 849	1 |- Fun recs ( F )

Syntax hints:   -> wi 4   /\ wa 97   A.wal 1241   = wceq 1243   E.wex 1381   e. wcel 1393   {cab 2026   A.wral 2306   E.wrex 2307   <.cop 3378   U.cuni 3580   class class class wbr 3764   Oncon0 4100   |` cres 4347   Rel wrel 4350   Fun wfun 4896   Fn wfn 4897   ` cfv 4902  recscrecs 5919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944  ax-setind 4262

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-mo 1904  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-sbc 2765  df-csb 2853  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-iun 3659  df-br 3765  df-opab 3819  df-mpt 3820  df-tr 3855  df-id 4030  df-iord 4103  df-on 4105  df-xp 4351  df-rel 4352  df-cnv 4353  df-co 4354  df-dm 4355  df-res 4357  df-iota 4867  df-fun 4904  df-fn 4905  df-fv 4910  df-recs 5920

This theorem is referenced by:  tfrlem9  5935  tfrlemibfn  5942  tfrlemiubacc  5944  tfri1d  5949  tfrfun  5955  rdgfun  5960