Theorem tfrlem7 3908

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 3520	. 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 3907	. 2 |- Rel F
5	3	eleq2i 1535	. . . . . . . 8 |- (<.x, u>. e. F <-> <.x, u>. e. U.A)
6		eluni 2501	. . . . . . . 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 1535	. . . . . . . 8 |- (<.x, v>. e. F <-> <.x, v>. e. U.A)
9		eluni 2501	. . . . . . . 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 482	. . . . . 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 1321	. . . . . 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 506	. . . . . . . 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 3906	. . . . . . . 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 1294	. . . . 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 961	. . 3 |- A.v((<.x, u>. e. F /\ <.x, v>. e. F) -> u = v)
23	22	gen2 981	. 2 |- A.xA.uA.v((<.x, u>. e. F /\ <.x, v>. e. F) -> u = v)
24	1, 4, 23	mpbir2an 729	1 |- Fun F

Syntax hints:   -> wi 3   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  E.wex 978  {cab 1461  A.wral 1642  E.wrex 1643  <.cop 2407  U.cuni 2498  Oncon0 2943   |` cres 3167  Rel wrel 3170  Fun wfun 3171   Fn wfn 3172  ` cfv 3177

This theorem is referenced by:  tfrlem9 3910  tfrlem10 3911  tfr1 3915  numthlem 4763  zorn2lem1 4768  zorn2lem2 4769  zorn2lem5 4772  zorn2lem7 4774

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-sep 2698  ax-pow 2737  ax-pr 2774  ax-un 2861

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-rab 1649  df-v 1808  df-sbc 1938  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-nul 2277  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-fv 3193

Copyright terms: Public domain