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

Proof

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