Metamath Proof Explorer


Theorem fununi

Description: The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004)

Ref Expression
Assertion fununi f A Fun f g A f g g f Fun A

Proof

Step Hyp Ref Expression
1 funrel Fun f Rel f
2 1 adantr Fun f g A f g g f Rel f
3 2 ralimi f A Fun f g A f g g f f A Rel f
4 reluni Rel A f A Rel f
5 3 4 sylibr f A Fun f g A f g g f Rel A
6 r19.28v Fun f g A f g g f g A Fun f f g g f
7 6 ralimi f A Fun f g A f g g f f A g A Fun f f g g f
8 ssel w v x y w x y v
9 8 anim1d w v x y w x z v x y v x z v
10 dffun4 Fun v Rel v x y z x y v x z v y = z
11 10 simprbi Fun v x y z x y v x z v y = z
12 11 19.21bbi Fun v z x y v x z v y = z
13 12 19.21bi Fun v x y v x z v y = z
14 9 13 syl9r Fun v w v x y w x z v y = z
15 14 adantl Fun w Fun v w v x y w x z v y = z
16 ssel v w x z v x z w
17 16 anim2d v w x y w x z v x y w x z w
18 dffun4 Fun w Rel w x y z x y w x z w y = z
19 18 simprbi Fun w x y z x y w x z w y = z
20 19 19.21bbi Fun w z x y w x z w y = z
21 20 19.21bi Fun w x y w x z w y = z
22 17 21 syl9r Fun w v w x y w x z v y = z
23 22 adantr Fun w Fun v v w x y w x z v y = z
24 15 23 jaod Fun w Fun v w v v w x y w x z v y = z
25 24 imp Fun w Fun v w v v w x y w x z v y = z
26 25 2ralimi w A v A Fun w Fun v w v v w w A v A x y w x z v y = z
27 funeq f = w Fun f Fun w
28 sseq1 f = w f g w g
29 sseq2 f = w g f g w
30 28 29 orbi12d f = w f g g f w g g w
31 27 30 anbi12d f = w Fun f f g g f Fun w w g g w
32 sseq2 g = v w g w v
33 sseq1 g = v g w v w
34 32 33 orbi12d g = v w g g w w v v w
35 34 anbi2d g = v Fun w w g g w Fun w w v v w
36 31 35 cbvral2vw f A g A Fun f f g g f w A v A Fun w w v v w
37 ralcom f A g A Fun f f g g f g A f A Fun f f g g f
38 orcom f g g f g f f g
39 sseq1 g = w g f w f
40 sseq2 g = w f g f w
41 39 40 orbi12d g = w g f f g w f f w
42 38 41 syl5bb g = w f g g f w f f w
43 42 anbi2d g = w Fun f f g g f Fun f w f f w
44 funeq f = v Fun f Fun v
45 sseq2 f = v w f w v
46 sseq1 f = v f w v w
47 45 46 orbi12d f = v w f f w w v v w
48 44 47 anbi12d f = v Fun f w f f w Fun v w v v w
49 43 48 cbvral2vw g A f A Fun f f g g f w A v A Fun v w v v w
50 37 49 bitri f A g A Fun f f g g f w A v A Fun v w v v w
51 36 50 anbi12i f A g A Fun f f g g f f A g A Fun f f g g f w A v A Fun w w v v w w A v A Fun v w v v w
52 anidm f A g A Fun f f g g f f A g A Fun f f g g f f A g A Fun f f g g f
53 anandir Fun w Fun v w v v w Fun w w v v w Fun v w v v w
54 53 2ralbii w A v A Fun w Fun v w v v w w A v A Fun w w v v w Fun v w v v w
55 r19.26-2 w A v A Fun w w v v w Fun v w v v w w A v A Fun w w v v w w A v A Fun v w v v w
56 54 55 bitr2i w A v A Fun w w v v w w A v A Fun v w v v w w A v A Fun w Fun v w v v w
57 51 52 56 3bitr3i f A g A Fun f f g g f w A v A Fun w Fun v w v v w
58 eluni x y A w x y w w A
59 eluni x z A v x z v v A
60 58 59 anbi12i x y A x z A w x y w w A v x z v v A
61 exdistrv w v x y w w A x z v v A w x y w w A v x z v v A
62 an4 x y w w A x z v v A x y w x z v w A v A
63 62 biancomi x y w w A x z v v A w A v A x y w x z v
64 63 2exbii w v x y w w A x z v v A w v w A v A x y w x z v
65 60 61 64 3bitr2i x y A x z A w v w A v A x y w x z v
66 65 imbi1i x y A x z A y = z w v w A v A x y w x z v y = z
67 19.23v w v w A v A x y w x z v y = z w v w A v A x y w x z v y = z
68 r2al w A v A x y w x z v y = z w v w A v A x y w x z v y = z
69 impexp w A v A x y w x z v y = z w A v A x y w x z v y = z
70 69 2albii w v w A v A x y w x z v y = z w v w A v A x y w x z v y = z
71 19.23v v w A v A x y w x z v y = z v w A v A x y w x z v y = z
72 71 albii w v w A v A x y w x z v y = z w v w A v A x y w x z v y = z
73 68 70 72 3bitr2ri w v w A v A x y w x z v y = z w A v A x y w x z v y = z
74 66 67 73 3bitr2i x y A x z A y = z w A v A x y w x z v y = z
75 26 57 74 3imtr4i f A g A Fun f f g g f x y A x z A y = z
76 75 alrimiv f A g A Fun f f g g f z x y A x z A y = z
77 76 alrimivv f A g A Fun f f g g f x y z x y A x z A y = z
78 7 77 syl f A Fun f g A f g g f x y z x y A x z A y = z
79 dffun4 Fun A Rel A x y z x y A x z A y = z
80 5 78 79 sylanbrc f A Fun f g A f g g f Fun A