Theorem fununi 4582

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		funrel 4542	. . . . 5 |- (Fun f -> Rel f)
2	1	adantr 447	. . . 4 |- ((Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Rel f)
3	2	ralimi 2418	. . 3 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> A.f e. A Rel f)
4		reluni 4233	. . 3 |- (Rel U.A <-> A.f e. A Rel f)
5	3, 4	sylibr 243	. 2 |- (A.f e. A (Fun f /\ A.g e. A (f C_ g \/ g C_ f)) -> Rel U.A)
6		r19.28av 2473	. . . 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)))
7	6	ralimi 2418	. . 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)))
8		ssel 2846	. . . . . . . . . . . . 13 |- (w C_ v -> (<.x, y>. e. w -> <.x, y>. e. v))
9	8	anim1d 534	. . . . . . . . . . . 12 |- (w C_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> (<.x, y>. e. v /\ <.x, z>. e. v)))
10		dffun4 4537	. . . . . . . . . . . . . 14 |- (Fun v <-> (Rel v /\ A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z)))
11	10	simprbi 446	. . . . . . . . . . . . 13 |- (Fun v -> A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
12		ax-4 1608	. . . . . . . . . . . . . 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))
13	12	a4s 1619	. . . . . . . . . . . . 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))
14		ax-4 1608	. . . . . . . . . . . . 13 |- (A.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z) -> ((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
15	11, 13, 14	3syl 41	. . . . . . . . . . . 12 |- (Fun v -> ((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
16	9, 15	syl9r 58	. . . . . . . . . . 11 |- (Fun v -> (w C_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
17	16	adantl 448	. . . . . . . . . 10 |- ((Fun w /\ Fun v) -> (w C_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
18		ssel 2846	. . . . . . . . . . . . 13 |- (v C_ w -> (<.x, z>. e. v -> <.x, z>. e. w))
19	18	anim2d 535	. . . . . . . . . . . 12 |- (v C_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> (<.x, y>. e. w /\ <.x, z>. e. w)))
20		dffun4 4537	. . . . . . . . . . . . . 14 |- (Fun w <-> (Rel w /\ A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z)))
21	20	simprbi 446	. . . . . . . . . . . . 13 |- (Fun w -> A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
22		ax-4 1608	. . . . . . . . . . . . . 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))
23	22	a4s 1619	. . . . . . . . . . . . 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))
24		ax-4 1608	. . . . . . . . . . . . 13 |- (A.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z) -> ((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
25	21, 23, 24	3syl 41	. . . . . . . . . . . 12 |- (Fun w -> ((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
26	19, 25	syl9r 58	. . . . . . . . . . 11 |- (Fun w -> (v C_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
27	26	adantr 447	. . . . . . . . . 10 |- ((Fun w /\ Fun v) -> (v C_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
28	17, 27	jaod 454	. . . . . . . . 9 |- ((Fun w /\ Fun v) -> ((w C_ v \/ v C_ w) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
29	28	imp 393	. . . . . . . 8 |- (((Fun w /\ Fun v) /\ (w C_ v \/ v C_ w)) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
30	29	ralimi 2418	. . . . . . 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))
31	30	ralimi 2418	. . . . . 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))
32		funeq 4544	. . . . . . . . . 10 |- (f = w -> (Fun f <-> Fun w))
33		sseq1 2865	. . . . . . . . . . 11 |- (f = w -> (f C_ g <-> w C_ g))
34		sseq2 2866	. . . . . . . . . . 11 |- (f = w -> (g C_ f <-> g C_ w))
35	33, 34	orbi12d 762	. . . . . . . . . 10 |- (f = w -> ((f C_ g \/ g C_ f) <-> (w C_ g \/ g C_ w)))
36	32, 35	anbi12d 763	. . . . . . . . 9 |- (f = w -> ((Fun f /\ (f C_ g \/ g C_ f)) <-> (Fun w /\ (w C_ g \/ g C_ w))))
37		sseq2 2866	. . . . . . . . . . 11 |- (g = v -> (w C_ g <-> w C_ v))
38		sseq1 2865	. . . . . . . . . . 11 |- (g = v -> (g C_ w <-> v C_ w))
39	37, 38	orbi12d 762	. . . . . . . . . 10 |- (g = v -> ((w C_ g \/ g C_ w) <-> (w C_ v \/ v C_ w)))
40	39	anbi2d 751	. . . . . . . . 9 |- (g = v -> ((Fun w /\ (w C_ g \/ g C_ w)) <-> (Fun w /\ (w C_ v \/ v C_ w))))
41	36, 40	cbvral2v 2529	. . . . . . . 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)))
42		ralcom 2488	. . . . . . . . 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)))
43		orcom 466	. . . . . . . . . . . 12 |- ((f C_ g \/ g C_ f) <-> (g C_ f \/ f C_ g))
44		sseq1 2865	. . . . . . . . . . . . 13 |- (g = w -> (g C_ f <-> w C_ f))
45		sseq2 2866	. . . . . . . . . . . . 13 |- (g = w -> (f C_ g <-> f C_ w))
46	44, 45	orbi12d 762	. . . . . . . . . . . 12 |- (g = w -> ((g C_ f \/ f C_ g) <-> (w C_ f \/ f C_ w)))
47	43, 46	syl5bb 721	. . . . . . . . . . 11 |- (g = w -> ((f C_ g \/ g C_ f) <-> (w C_ f \/ f C_ w)))
48	47	anbi2d 751	. . . . . . . . . 10 |- (g = w -> ((Fun f /\ (f C_ g \/ g C_ f)) <-> (Fun f /\ (w C_ f \/ f C_ w))))
49		funeq 4544	. . . . . . . . . . 11 |- (f = v -> (Fun f <-> Fun v))
50		sseq2 2866	. . . . . . . . . . . 12 |- (f = v -> (w C_ f <-> w C_ v))
51		sseq1 2865	. . . . . . . . . . . 12 |- (f = v -> (f C_ w <-> v C_ w))
52	50, 51	orbi12d 762	. . . . . . . . . . 11 |- (f = v -> ((w C_ f \/ f C_ w) <-> (w C_ v \/ v C_ w)))
53	49, 52	anbi12d 763	. . . . . . . . . 10 |- (f = v -> ((Fun f /\ (w C_ f \/ f C_ w)) <-> (Fun v /\ (w C_ v \/ v C_ w))))
54	48, 53	cbvral2v 2529	. . . . . . . . 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)))
55	42, 54	bitri 279	. . . . . . . 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)))
56	41, 55	anbi12i 710	. . . . . . 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))))
57		anidm 624	. . . . . . 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)))
58		anandir 888	. . . . . . . . 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))))
59	58	2ralbii 2379	. . . . . . . 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))))
60		r19.26-2 2468	. . . . . . . 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))))
61	59, 60	bitr2i 281	. . . . . . 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)))
62	56, 57, 61	3bitr3i 293	. . . . . 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)))
63		eluni 3369	. . . . . . . . . 10 |- (<.x, y>. e. U.A <-> E.w(<.x, y>. e. w /\ w e. A))
64		eluni 3369	. . . . . . . . . 10 |- (<.x, z>. e. U.A <-> E.v(<.x, z>. e. v /\ v e. A))
65	63, 64	anbi12i 710	. . . . . . . . 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)))
66		eeanv 1974	. . . . . . . . 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)))
67		an4 882	. . . . . . . . . . 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)))
68		ancom 414	. . . . . . . . . . 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)))
69	67, 68	bitri 279	. . . . . . . . . 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)))
70	69	2exbii 1688	. . . . . . . . 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)))
71	65, 66, 70	3bitr2i 291	. . . . . . . 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)))
72	71	imbi1i 299	. . . . . . 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))
73		19.23v 1941	. . . . . . . . 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))
74	73	albii 1635	. . . . . . . 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))
75		impexp 404	. . . . . . . . . 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)))
76	75	2albii 1636	. . . . . . . . 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)))
77		r2al 2386	. . . . . . . . 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)))
78	76, 77	bitr4i 283	. . . . . . . 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))
79		19.23v 1941	. . . . . . . 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))
80	74, 78, 79	3bitr3ri 294	. . . . . . 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))
81	72, 80	bitri 279	. . . . . 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))
82	31, 62, 81	3imtr4i 328	. . . . 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))
83	82	19.21aiv 1933	. . . 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))
84	83	19.21aivv 1934	. . 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))
85	7, 84	syl 13	. 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))
86		dffun4 4537	. 2 |- (Fun U.A <-> (Rel U.A /\ A.xA.yA.z((<.x, y>. e. U.A /\ <.x, z>. e. U.A) -> y = z)))
87	5, 85, 86	sylanbrc 664	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 336   /\ wa 337  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615  A.wral 2355   C_ wss 2827  <.cop 3240  U.cuni 3366  Rel wrel 4124  Fun wfun 4125

This theorem is referenced by:  funcnvuni 4583  fun11uni 4584  axdc3lem2 6306  axfelem20 14718

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-iun 3438  df-br 3508  df-opab 3566  df-id 3747  df-rel 4134  df-cnv 4135  df-co 4136  df-fun 4141

Copyright terms: Public domain