Theorem tfrlem7 3902

Description: Lemma for transfinite recursion. The union of all acceptable functions is a function.

Hypotheses

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

Assertion

Ref	Expression
tfrlem7	|- Fun F

Distinct variable groups:   x,y,f,A   x,F,y,f   x,G,y,f

Proof of Theorem tfrlem7

Step	Hyp	Ref	Expression
1		dffun4 3514	. 2 |- (Fun F <-> (Rel F /\ A.xA.uA.v((<.x, u>. e. F /\ <.x, v>. e. F) -> u = v)))
2		tfrlem.1	. . 3 |- A = {f | E.x e. On (f Fn x /\ A.y e. x (f` y) = (G` (f |` y)))}
3		tfrlem.2	. . 3 |- F = U.A
4	2, 3	tfrlem6 3901	. 2 |- Rel F
5	3	eleq2i 1530	. . . . . . . 8 |- (<.x, u>. e. F <-> <.x, u>. e. U.A)
6		eluni 2496	. . . . . . . 8 |- (<.x, u>. e. U.A <-> E.g(<.x, u>. e. g /\ g e. A))
7	5, 6	bitr 173	. . . . . . 7 |- (<.x, u>. e. F <-> E.g(<.x, u>. e. g /\ g e. A))
8	3	eleq2i 1530	. . . . . . . 8 |- (<.x, v>. e. F <-> <.x, v>. e. U.A)
9		eluni 2496	. . . . . . . 8 |- (<.x, v>. e. U.A <-> E.h(<.x, v>. e. h /\ h e. A))
10	8, 9	bitr 173	. . . . . . 7 |- (<.x, v>. e. F <-> E.h(<.x, v>. e. h /\ h e. A))
11	7, 10	anbi12i 481	. . . . . 6 |- ((<.x, u>. e. F /\ <.x, v>. e. F) <-> (E.g(<.x, u>. e. g /\ g e. A) /\ E.h(<.x, v>. e. h /\ h e. A)))
12		eeanv 1318	. . . . . 6 |- (E.gE.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)))
13	11, 12	bitr4 176	. . . . 5 |- ((<.x, u>. e. F /\ <.x, v>. e. F) <-> E.gE.h((<.x, u>. e. g /\ g e. A) /\ (<.x, v>. e. h /\ h e. A)))
14		an4 505	. . . . . . . 8 |- (((<.x, u>. e. g /\ g e. A) /\ (<.x, v>. e. h /\ h e. A)) <-> ((<.x, u>. e. g /\ <.x, v>. e. h) /\ (g e. A /\ h e. A)))
15		ancom 435	. . . . . . . 8 |- (((<.x, u>. e. g /\ <.x, v>. e. h) /\ (g e. A /\ h e. A)) <-> ((g e. A /\ h e. A) /\ (<.x, u>. e. g /\ <.x, v>. e. h)))
16	14, 15	bitr 173	. . . . . . 7 |- (((<.x, u>. e. g /\ g e. A) /\ (<.x, v>. e. h /\ h e. A)) <-> ((g e. A /\ h e. A) /\ (<.x, u>. e. g /\ <.x, v>. e. h)))
17	2, 3	tfrlem5 3900	. . . . . . . 8 |- ((g e. A /\ h e. A) -> ((<.x, u>. e. g /\ <.x, v>. e. h) -> u = v))
18	17	imp 350	. . . . . . 7 |- (((g e. A /\ h e. A) /\ (<.x, u>. e. g /\ <.x, v>. e. h)) -> u = v)
19	16, 18	sylbi 199	. . . . . 6 |- (((<.x, u>. e. g /\ g e. A) /\ (<.x, v>. e. h /\ h e. A)) -> u = v)
20	19	19.23aivv 1291	. . . . 5 |- (E.gE.h((<.x, u>. e. g /\ g e. A) /\ (<.x, v>. e. h /\ h e. A)) -> u = v)
21	13, 20	sylbi 199	. . . 4 |- ((<.x, u>. e. F /\ <.x, v>. e. F) -> u = v)
22	21	ax-gen 960	. . 3 |- A.v((<.x, u>. e. F /\ <.x, v>. e. F) -> u = v)
23	22	gen2 980	. 2 |- A.xA.uA.v((<.x, u>. e. F /\ <.x, v>. e. F) -> u = v)
24	1, 4, 23	mpbir2an 728	1 |- Fun F

Syntax hints:   -> wi 3   /\ wa 223  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  {cab 1456  A.wral 1637  E.wrex 1638  <.cop 2401  U.cuni 2493  Oncon0 2938   |` cres 3162  Rel wrel 3165  Fun wfun 3166   Fn wfn 3167  ` cfv 3172

This theorem is referenced by:  tfrlem9 3904  tfrlem10 3905  tfr1 3909  numthlem 4755  zorn2lem1 4760  zorn2lem2 4761  zorn2lem5 4764  zorn2lem7 4766

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 774  df-3an 775  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-ral 1641  df-rex 1642  df-rab 1644  df-v 1803  df-sbc 1932  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-tp 2405  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-tr 2671  df-eprel 2821  df-id 2824  df-po 2831  df-so 2841  df-fr 2907  df-we 2924  df-ord 2941  df-on 2942  df-xp 3174  df-rel 3175  df-cnv 3176  df-co 3177  df-dm 3178  df-rn 3179  df-res 3180  df-ima 3181  df-fun 3182  df-fn 3183  df-fv 3188

Copyright terms: Public domain