Theorem fununi 4481

Description: The union of a chain (with respect to inclusion) of functions is a function.

Assertion

Ref	Expression
fununi	|- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Fun U.A)

Distinct variable group:   f,g,A

Proof of Theorem fununi

Step	Hyp	Ref	Expression
1		dffun4 4433	. 2 |- (Fun U.A <-> (Rel U.A /\ A.xA.yA.z((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z)))
2		funrel 4438	. . . . 5 |- (Fun f -> Rel f)
3	2	adantr 425	. . . 4 |- ((Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Rel f)
4	3	ralimi 2168	. . 3 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.f e. A Rel f)
5		reluni 4103	. . 3 |- (Rel U.A <-> A.f e. A Rel f)
6	4, 5	sylibr 217	. 2 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Rel U.A)
7		r19.28av 2226	. . . 4 |- ((Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.g e. A (Fun f /\ (f C_ g \/ g C_ f)))
8	7	ralimi 2168	. . 3 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)))
9		ssel 2615	. . . . . . . . . . . . 13 |- (w C_ v -> (<.x, y>. e. w -> <.x, y>. e. v))
10	9	anim1d 619	. . . . . . . . . . . 12 |- (w C_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> (<.x, y>. e. v /\ <.x, z>. e. v)))
11		dffun4 4433	. . . . . . . . . . . . . 14 |- (Fun v <-> (Rel v /\ A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z)))
12	11	simprbi 353	. . . . . . . . . . . . 13 |- (Fun v -> A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
13		ax-4 1319	. . . . . . . . . . . . . 14 |- (A.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z) -> A.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
14	13	a4s 1330	. . . . . . . . . . . . 13 |- (A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z) -> A.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
15		ax-4 1319	. . . . . . . . . . . . 13 |- (A.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z) -> ((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
16	12, 14, 15	3syl 24	. . . . . . . . . . . 12 |- (Fun v -> ((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
17	10, 16	syl9r 72	. . . . . . . . . . 11 |- (Fun v -> (w C_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
18	17	adantl 424	. . . . . . . . . 10 |- ((Fun w /\ Fun v) -> (w C_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
19		ssel 2615	. . . . . . . . . . . . 13 |- (v C_ w -> (<.x, z>. e. v -> <.x, z>. e. w))
20	19	anim2d 620	. . . . . . . . . . . 12 |- (v C_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> (<.x, y>. e. w /\ <.x, z>. e. w)))
21		dffun4 4433	. . . . . . . . . . . . . 14 |- (Fun w <-> (Rel w /\ A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z)))
22	21	simprbi 353	. . . . . . . . . . . . 13 |- (Fun w -> A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
23		ax-4 1319	. . . . . . . . . . . . . 14 |- (A.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z) -> A.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
24	23	a4s 1330	. . . . . . . . . . . . 13 |- (A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z) -> A.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
25		ax-4 1319	. . . . . . . . . . . . 13 |- (A.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z) -> ((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
26	22, 24, 25	3syl 24	. . . . . . . . . . . 12 |- (Fun w -> ((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
27	20, 26	syl9r 72	. . . . . . . . . . 11 |- (Fun w -> (v C_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
28	27	adantr 425	. . . . . . . . . 10 |- ((Fun w /\ Fun v) -> (v C_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
29	18, 28	jaod 469	. . . . . . . . 9 |- ((Fun w /\ Fun v) -> ((w C_ v \/ v C_ w) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
30	29	imp 377	. . . . . . . 8 |- (((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
31	30	ralimi 2168	. . . . . . 7 |- (A.v e. A ((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)) -> A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
32	31	ralimi 2168	. . . . . 6 |- (A.w e. A A.v e. A ((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)) -> A.w e. A A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
33		funeq 4441	. . . . . . . . . 10 |- (f = w -> (Fun f <-> Fun w))
34		sseq1 2637	. . . . . . . . . . 11 |- (f = w -> (f C_ g <-> w C_ g))
35		sseq2 2639	. . . . . . . . . . 11 |- (f = w -> (g C_ f <-> g C_ w))
36	34, 35	orbi12d 689	. . . . . . . . . 10 |- (f = w -> ((f C_ g \/ g C_ f) <-> (w C_ g \/ g C_ w)))
37	33, 36	anbi12d 690	. . . . . . . . 9 |- (f = w -> ((Fun f /\ (f C_ g \/ g C_ f)) <-> (Fun w /\ (w C_ g \/ g C_ w))))
38		sseq2 2639	. . . . . . . . . . 11 |- (g = v -> (w C_ g <-> w C_ v))
39		sseq1 2637	. . . . . . . . . . 11 |- (g = v -> (g C_ w <-> v C_ w))
40	38, 39	orbi12d 689	. . . . . . . . . 10 |- (g = v -> ((w C_ g \/ g C_ w) <-> (w C_ v \/ v C_ w)))
41	40	anbi2d 678	. . . . . . . . 9 |- (g = v -> ((Fun w /\ (w C_ g \/ g C_ w)) <-> (Fun w /\ (w C_ v \/ v C_ w))))
42	37, 41	cbvral2v 2283	. . . . . . . 8 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) <-> A.w e. A A.v e. A (Fun w /\ (w C_ v \/ v C_ w)))
43		ralcom 2242	. . . . . . . . 9 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) <-> A.g e. A A.f e. A (Fun f /\ (f C_ g \/ g C_ f)))
44		sseq1 2637	. . . . . . . . . . . . 13 |- (g = w -> (g C_ f <-> w C_ f))
45		sseq2 2639	. . . . . . . . . . . . 13 |- (g = w -> (f C_ g <-> f C_ w))
46	44, 45	orbi12d 689	. . . . . . . . . . . 12 |- (g = w -> ((g C_ f \/ f C_ g) <-> (w C_ f \/ f C_ w)))
47		orcom 266	. . . . . . . . . . . 12 |- ((f C_ g \/ g C_ f) <-> (g C_ f \/ f C_ g))
48	46, 47	syl5bb 591	. . . . . . . . . . 11 |- (g = w -> ((f C_ g \/ g C_ f) <-> (w C_ f \/ f C_ w)))
49	48	anbi2d 678	. . . . . . . . . 10 |- (g = w -> ((Fun f /\ (f C_ g \/ g C_ f)) <-> (Fun f /\ (w C_ f \/ f C_ w))))
50		funeq 4441	. . . . . . . . . . 11 |- (f = v -> (Fun f <-> Fun v))
51		sseq2 2639	. . . . . . . . . . . 12 |- (f = v -> (w C_ f <-> w C_ v))
52		sseq1 2637	. . . . . . . . . . . 12 |- (f = v -> (f C_ w <-> v C_ w))
53	51, 52	orbi12d 689	. . . . . . . . . . 11 |- (f = v -> ((w C_ f \/ f C_ w) <-> (w C_ v \/ v C_ w)))
54	50, 53	anbi12d 690	. . . . . . . . . 10 |- (f = v -> ((Fun f /\ (w C_ f \/ f C_ w)) <-> (Fun v /\ (w C_ v \/ v C_ w))))
55	49, 54	cbvral2v 2283	. . . . . . . . 9 |- (A.g e. A A.f e. A (Fun f /\ (f C_ g \/ g C_ f)) <-> A.w e. A A.v e. A (Fun v /\ (w C_ v \/ v C_ w)))
56	43, 55	bitri 190	. . . . . . . 8 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) <-> A.w e. A A.v e. A (Fun v /\ (w C_ v \/ v C_ w)))
57	42, 56	anbi12i 540	. . . . . . 7 |- ((A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) /\ A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f))) <-> (A.w e. A A.v e. A (Fun w /\ (w C_ v \/ v C_ w)) /\ A.w e. A A.v e. A (Fun v /\ (w C_ v \/ v C_ w))))
58		anidm 478	. . . . . . 7 |- ((A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) /\ A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f))) <-> A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)))
59		anandir 569	. . . . . . . . 9 |- (((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)) <-> ((Fun w /\ (w C_ v \/ v C_ w)) /\ (Fun v /\ (w C_ v \/ v C_ w))))
60	59	2ralbii 2129	. . . . . . . 8 |- (A.w e. A A.v e. A ((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)) <-> A.w e. A A.v e. A ((Fun w /\ (w C_ v \/ v C_ w)) /\ (Fun v /\ (w C_ v \/ v C_ w))))
61		r19.26-2 2221	. . . . . . . 8 |- (A.w e. A A.v e. A ((Fun w /\ (w C_ v \/ v C_ w)) /\ (Fun v /\ (w C_ v \/ v C_ w))) <-> (A.w e. A A.v e. A (Fun w /\ (w C_ v \/ v C_ w)) /\ A.w e. A A.v e. A (Fun v /\ (w C_ v \/ v C_ w))))
62	60, 61	bitr2i 191	. . . . . . 7 |- ((A.w e. A A.v e. A (Fun w /\ (w C_ v \/ v C_ w)) /\ A.w e. A A.v e. A (Fun v /\ (w C_ v \/ v C_ w))) <-> A.w e. A A.v e. A ((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)))
63	57, 58, 62	3bitr3i 198	. . . . . 6 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) <-> A.w e. A A.v e. A ((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)))
64		eluni 3180	. . . . . . . . . 10 |- (<.x, y>. e. U.A <-> E.w(<.x, y>. e. w /\ w e. A))
65		eluni 3180	. . . . . . . . . 10 |- (<.x, z>. e. U.A <-> E.v(<.x, z>. e. v /\ v e. A))
66	64, 65	anbi12i 540	. . . . . . . . 9 |- ((<.x, y>. e. U.A /\ <.x, z>. e. U.A) <-> (E.w(<.x, y>. e. w /\ w e. A) /\ E.v(<.x, z>. e. v /\ v e. A)))
67		eeanv 1707	. . . . . . . . 9 |- (E.wE.v((<.x, y>. e. w /\ w e. A) /\ (<.x, z>. e. v /\ v e. A)) <-> (E.w(<.x, y>. e. w /\ w e. A) /\ E.v(<.x, z>. e. v /\ v e. A)))
68		an4 564	. . . . . . . . . . 11 |- (((<.x, y>. e. w /\ w e. A) /\ (<.x, z>. e. v /\ v e. A)) <-> ((<.x, y>. e. w /\ <.x, z>. e. v) /\ (w e. A /\ v e. A)))
69		ancom 482	. . . . . . . . . . 11 |- (((<.x, y>. e. w /\ <.x, z>. e. v) /\ (w e. A /\ v e. A)) <-> ((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)))
70	68, 69	bitri 190	. . . . . . . . . 10 |- (((<.x, y>. e. w /\ w e. A) /\ (<.x, z>. e. v /\ v e. A)) <-> ((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)))
71	70	2exbii 1399	. . . . . . . . 9 |- (E.wE.v((<.x, y>. e. w /\ w e. A) /\ (<.x, z>. e. v /\ v e. A)) <-> E.wE.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)))
72	66, 67, 71	3bitr2i 196	. . . . . . . 8 |- ((<.x, y>. e. U.A /\ <.x, z>. e. U.A) <-> E.wE.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)))
73	72	imbi1i 203	. . . . . . 7 |- (((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z) <-> (E.wE.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z))
74		19.23v 1672	. . . . . . . . 9 |- (A.v(((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> (E.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z))
75	74	albii 1346	. . . . . . . 8 |- (A.wA.v(((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> A.w(E.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z))
76		impexp 374	. . . . . . . . . 10 |- ((((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> ((w e. A /\ v e. A) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
77	76	2albii 1347	. . . . . . . . 9 |- (A.wA.v(((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> A.wA.v((w e. A /\ v e. A) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
78		r2al 2136	. . . . . . . . 9 |- (A.w e. A A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z) <-> A.wA.v((w e. A /\ v e. A) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
79	77, 78	bitr4i 193	. . . . . . . 8 |- (A.wA.v(((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> A.w e. A A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
80		19.23v 1672	. . . . . . . 8 |- (A.w(E.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> (E.wE.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z))
81	75, 79, 80	3bitr3ri 199	. . . . . . 7 |- ((E.wE.v((w e. A /\ v e. A) /\ (<.x, y>. e. w /\ <.x, z>. e. v)) -> y = z) <-> A.w e. A A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
82	73, 81	bitri 190	. . . . . 6 |- (((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z) <-> A.w e. A A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
83	32, 63, 82	3imtr4i 236	. . . . 5 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) -> ((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z))
84	83	19.21aiv 1664	. . . 4 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) -> A.z((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z))
85	84	19.21aivv 1665	. . 3 |- (A.f e. A A.g e. A (Fun f /\ (f C_ g \/ g C_ f)) -> A.xA.yA.z((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z))
86	8, 85	syl 12	. 2 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.xA.yA.z((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z))
87	1, 6, 86	sylanbrc 527	1 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Fun U.A)

Syntax hints:   -> wi 3   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105   C_ wss 2593  <.cop 3046  U.cuni 3177  Rel wrel 3991  Fun wfun 3992

This theorem is referenced by:  funcnvuni 4482  fun11uni 4483  axfelem16 14046

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-iun 3257  df-br 3339  df-opab 3396  df-id 3586  df-rel 4001  df-cnv 4002  df-co 4003  df-fun 4008

Copyright terms: Public domain