Theorem fununi 3555

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 (_ g \/ g (_ f)) -> Fun U.A)

Distinct variable group:   f,g,A

Proof of Theorem fununi

Step	Hyp	Ref	Expression
1		funrel 3525	. . . . . 6 |- (Fun f -> Rel f)
2	1	adantr 389	. . . . 5 |- ((Fun f /\ A.g e. A (f (_ g \/ g (_ f)) -> Rel f)
3	2	r19.20si 1703	. . . 4 |- (A.f e. A (Fun f /\ A.g e. A (f (_ g \/ g (_ f)) -> A.f e. A Rel f)
4		reluni 3260	. . . 4 |- (Rel U.A <-> A.f e. A Rel f)
5	3, 4	sylibr 200	. . 3 |- (A.f e. A (Fun f /\ A.g e. A (f (_ g \/ g (_ f)) -> Rel U.A)
6		r19.28av 1752	. . . . 5 |- ((Fun f /\ A.g e. A (f (_ g \/ g (_ f)) -> A.g e. A (Fun f /\ (f (_ g \/ g (_ f)))
7	6	r19.20si 1703	. . . 4 |- (A.f e. A (Fun f /\ A.g e. A (f (_ g \/ g (_ f)) -> A.f e. A A.g e. A (Fun f /\ (f (_ g \/ g (_ f)))
8		ssel 2059	. . . . . . . . . . . . . 14 |- (w (_ v -> (<.x, y>. e. w -> <.x, y>. e. v))
9	8	anim1d 559	. . . . . . . . . . . . 13 |- (w (_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> (<.x, y>. e. v /\ <.x, z>. e. v)))
10		dffun4 3520	. . . . . . . . . . . . . . 15 |- (Fun v <-> (Rel v /\ A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z)))
11	10	pm3.27bi 326	. . . . . . . . . . . . . 14 |- (Fun v -> A.xA.yA.z((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
12		ax-4 971	. . . . . . . . . . . . . . 15 |- (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 982	. . . . . . . . . . . . . 14 |- (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 971	. . . . . . . . . . . . . 14 |- (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 20	. . . . . . . . . . . . 13 |- (Fun v -> ((<.x, y>. e. v /\ <.x, z>. e. v) -> y = z))
16	9, 15	syl9r 58	. . . . . . . . . . . 12 |- (Fun v -> (w (_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
17	16	adantl 388	. . . . . . . . . . 11 |- ((Fun w /\ Fun v) -> (w (_ v -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
18		ssel 2059	. . . . . . . . . . . . . 14 |- (v (_ w -> (<.x, z>. e. v -> <.x, z>. e. w))
19	18	anim2d 560	. . . . . . . . . . . . 13 |- (v (_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> (<.x, y>. e. w /\ <.x, z>. e. w)))
20		dffun4 3520	. . . . . . . . . . . . . . 15 |- (Fun w <-> (Rel w /\ A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z)))
21	20	pm3.27bi 326	. . . . . . . . . . . . . 14 |- (Fun w -> A.xA.yA.z((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
22		ax-4 971	. . . . . . . . . . . . . . 15 |- (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 982	. . . . . . . . . . . . . 14 |- (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 971	. . . . . . . . . . . . . 14 |- (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 20	. . . . . . . . . . . . 13 |- (Fun w -> ((<.x, y>. e. w /\ <.x, z>. e. w) -> y = z))
26	19, 25	syl9r 58	. . . . . . . . . . . 12 |- (Fun w -> (v (_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
27	26	adantr 389	. . . . . . . . . . 11 |- ((Fun w /\ Fun v) -> (v (_ w -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
28	17, 27	jaod 424	. . . . . . . . . 10 |- ((Fun w /\ Fun v) -> ((w (_ v \/ v (_ w) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z)))
29	28	imp 350	. . . . . . . . 9 |- (((Fun w /\ Fun v) /\ (w (_ v \/ v (_ w)) -> ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
30	29	r19.20si 1703	. . . . . . . 8 |- (A.v e. A ((Fun w /\ Fun v) /\ (w (_ v \/ v (_ w)) -> A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
31	30	r19.20si 1703	. . . . . . 7 |- (A.w e. A A.v e. A ((Fun w /\ Fun v) /\ (w (_ v \/ v (_ w)) -> A.w e. A A.v e. A ((<.x, y>. e. w /\ <.x, z>. e. v) -> y = z))
32		funeq 3527	. . . . . . . . . . 11 |- (f = w -> (Fun f <-> Fun w))
33		sseq1 2078	. . . . . . . . . . . 12 |- (f = w -> (f (_ g <-> w (_ g))
34		sseq2 2079	. . . . . . . . . . . 12 |- (f = w -> (g (_ f <-> g (_ w))
35	33, 34	orbi12d 626	. . . . . . . . . . 11 |- (f = w -> ((f (_ g \/ g (_ f) <-> (w (_ g \/ g (_ w)))
36	32, 35	anbi12d 627	. . . . . . . . . 10 |- (f = w -> ((Fun f /\ (f (_ g \/ g (_ f)) <-> (Fun w /\ (w (_ g \/ g (_ w))))
37		sseq2 2079	. . . . . . . . . . . 12 |- (g = v -> (w (_ g <-> w (_ v))
38		sseq1 2078	. . . . . . . . . . . 12 |- (g = v -> (g (_ w <-> v (_ w))
39	37, 38	orbi12d 626	. . . . . . . . . . 11 |- (g = v -> ((w (_ g \/ g (_ w) <-> (w (_ v \/ v (_ w)))
40	39	anbi2d 615	. . . . . . . . . 10 |- (g = v -> ((Fun w /\ (w (_ g \/ g (_ w)) <-> (Fun w /\ (w (_ v \/ v (_ w))))
41	36, 40	cbvral2v 1799	. . . . . . . . 9 |- (A.f e. A A.g e. A (Fun f /\ (f (_ g \/ g (_ f)) <-> A.w e. A A.v e. A (Fun w /\ (w (_ v \/ v (_ w)))
42		ralcom 1771	. . . . . . . . . 10 |- (A.f e. A A.g e. A (Fun f /\ (f (_ g \/ g (_ f)) <-> A.g e. A A.f e. A (Fun f /\ (f (_ g \/ g (_ f)))
43		sseq1 2078	. . . . . . . . . . . . . 14 |- (g = w -> (g (_ f <-> w (_ f))
44		sseq2 2079	. . . . . . . . . . . . . 14 |- (g = w -> (f (_ g <-> f (_ w))
45	43, 44	orbi12d 626	. . . . . . . . . . . . 13 |- (g = w -> ((g (_ f \/ f (_ g) <-> (w (_ f \/ f (_ w)))
46		orcom 246	. . . . . . . . . . . . 13 |- ((f (_ g \/ g (_ f) <-> (g (_ f \/ f (_ g))
47	45, 46	syl5bb 531	. . . . . . . . . . . 12 |- (g = w -> ((f (_ g \/ g (_ f) <-> (w (_ f \/ f (_ w)))
48	47	anbi2d 615	. . . . . . . . . . 11 |- (g = w -> ((Fun f /\ (f (_ g \/ g (_ f)) <-> (Fun f /\ (w (_ f \/ f (_ w))))
49		funeq 3527	. . . . . . . . . . . 12 |- (f = v -> (Fun f <-> Fun v))
50		sseq2 2079	. . . . . . . . . . . . 13 |- (f = v -> (w (_ f <-> w (_ v))
51		sseq1 2078	. . . . . . . . . . . . 13 |- (f = v -> (f (_ w <-> v (_ w))
52	50, 51	orbi12d 626	. . . . . . . . . . . 12 |- (f = v -> ((w (_ f \/ f (_ w) <-> (w (_ v \/ v (_ w)))
53	49, 52	anbi12d 627	. . . . . . . . . . 11 |- (f = v -> ((Fun f /\ (w (_ f \/ f (_ w)) <-> (Fun v /\ (w (_ v \/ v (_ w))))
54	48, 53	cbvral2v 1799	. . . . . . . . . 10 |- (A.g e. A A.f e. A (Fun f /\ (f (_ g \/ g (_ f)) <-> A.w e. A A.v e. A (Fun v /\ (w (_ v \/ v (_ w)))
55	42, 54	bitr 173	. . . . . . . . 9 |- (A.f e. A A.g e. A (Fun f /\ (f (_ g \/ g (_ f)) <-> A.w e. A A.v e. A (Fun v /\ (w (_ v \/ v (_ w)))
56	41, 55	anbi12i 482	. . . . . . . 8 |- ((A.f e. A A.g e. A (Fun f /\ (f (_ g \/ g (_ f)) /\ A.f e. A A.g e. A (Fun f /\ (f (_ g \/ g (_ f))) <-> (A.w e. A A.v e. A (Fun w /\ (w (_ v \/ v (_