ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fununi Structured version   Unicode version

Theorem fununi 4881
Description: The union of a chain (with respect to inclusion) of functions is a function. (Contributed by NM, 10-Aug-2004.)
Assertion
Ref Expression
fununi  Fun  C_  C_  Fun  U.
Distinct variable group:   ,,

Proof of Theorem fununi
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funrel 4833 . . . . 5  Fun  Rel
21adantr 261 . . . 4  Fun  C_  C_ 
Rel
32ralimi 2353 . . 3  Fun  C_  C_  Rel
4 reluni 4375 . . 3  Rel  U.  Rel
53, 4sylibr 137 . 2  Fun  C_  C_  Rel  U.
6 r19.28av 2418 . . . 4  Fun  C_  C_  Fun  C_  C_
76ralimi 2353 . . 3  Fun  C_  C_  Fun  C_  C_
8 ssel 2907 . . . . . . . . . . . . 13 
C_  <. ,  >.  <. ,  >.
98anim1d 319 . . . . . . . . . . . 12 
C_  <. , 
>.  <. ,  >.  <. ,  >.  <. , 
>.
10 dffun4 4828 . . . . . . . . . . . . . . 15  Fun  Rel  <. ,  >.  <. , 
>.
1110simprbi 260 . . . . . . . . . . . . . 14  Fun  <. , 
>.  <. ,  >.
121119.21bbi 1424 . . . . . . . . . . . . 13  Fun  <. , 
>.  <. ,  >.
131219.21bi 1423 . . . . . . . . . . . 12  Fun 
<. ,  >.  <. ,  >.
149, 13syl9r 67 . . . . . . . . . . 11  Fun 
C_  <. , 
>.  <. ,  >.
1514adantl 262 . . . . . . . . . 10  Fun  Fun  C_  <. , 
>.  <. ,  >.
16 ssel 2907 . . . . . . . . . . . . 13 
C_  <. ,  >.  <. ,  >.
1716anim2d 320 . . . . . . . . . . . 12 
C_  <. , 
>.  <. ,  >.  <. ,  >.  <. , 
>.
18 dffun4 4828 . . . . . . . . . . . . . . 15  Fun  Rel  <. ,  >.  <. , 
>.
1918simprbi 260 . . . . . . . . . . . . . 14  Fun 
<. ,  >.  <. ,  >.
201919.21bbi 1424 . . . . . . . . . . . . 13  Fun  <. , 
>.  <. ,  >.
212019.21bi 1423 . . . . . . . . . . . 12  Fun  <. ,  >.  <. , 
>.
2217, 21syl9r 67 . . . . . . . . . . 11  Fun  C_  <. ,  >.  <. , 
>.
2322adantr 261 . . . . . . . . . 10  Fun  Fun  C_  <. , 
>.  <. ,  >.
2415, 23jaod 621 . . . . . . . . 9  Fun  Fun  C_  C_  <. ,  >.  <. , 
>.
2524imp 115 . . . . . . . 8  Fun  Fun  C_  C_  <. , 
>.  <. ,  >.
2625ralimi 2353 . . . . . . 7  Fun  Fun  C_  C_  <. , 
>.  <. ,  >.
2726ralimi 2353 . . . . . 6  Fun  Fun  C_  C_  <. ,  >.  <. , 
>.
28 funeq 4835 . . . . . . . . . 10  Fun  Fun
29 sseq1 2934 . . . . . . . . . . 11  C_  C_
30 sseq2 2935 . . . . . . . . . . 11  C_  C_
3129, 30orbi12d 691 . . . . . . . . . 10  C_  C_  C_  C_
3228, 31anbi12d 442 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
33 sseq2 2935 . . . . . . . . . . 11  C_  C_
34 sseq1 2934 . . . . . . . . . . 11  C_  C_
3533, 34orbi12d 691 . . . . . . . . . 10  C_  C_  C_  C_
3635anbi2d 437 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
3732, 36cbvral2v 2510 . . . . . . . 8  Fun  C_  C_  Fun  C_  C_
38 ralcom 2442 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
39 orcom 631 . . . . . . . . . . . 12  C_  C_ 
C_  C_
40 sseq1 2934 . . . . . . . . . . . . 13  C_  C_
41 sseq2 2935 . . . . . . . . . . . . 13  C_  C_
4240, 41orbi12d 691 . . . . . . . . . . . 12  C_  C_  C_  C_
4339, 42syl5bb 181 . . . . . . . . . . 11  C_  C_  C_  C_
4443anbi2d 437 . . . . . . . . . 10  Fun  C_  C_  Fun 
C_  C_
45 funeq 4835 . . . . . . . . . . 11  Fun  Fun
46 sseq2 2935 . . . . . . . . . . . 12  C_  C_
47 sseq1 2934 . . . . . . . . . . . 12  C_  C_
4846, 47orbi12d 691 . . . . . . . . . . 11  C_  C_  C_  C_
4945, 48anbi12d 442 . . . . . . . . . 10  Fun  C_  C_  Fun 
C_  C_
5044, 49cbvral2v 2510 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
5138, 50bitri 173 . . . . . . . 8  Fun  C_  C_  Fun  C_  C_
5237, 51anbi12i 433 . . . . . . 7  Fun  C_  C_  Fun 
C_  C_  Fun  C_  C_  Fun  C_  C_
53 anidm 376 . . . . . . 7  Fun  C_  C_  Fun 
C_  C_  Fun  C_  C_
54 anandir 510 . . . . . . . . 9  Fun  Fun  C_  C_  Fun  C_  C_  Fun  C_  C_
55542ralbii 2301 . . . . . . . 8  Fun  Fun  C_  C_  Fun  C_  C_  Fun 
C_  C_
56 r19.26-2 2411 . . . . . . . 8  Fun  C_  C_  Fun 
C_  C_  Fun  C_  C_  Fun  C_  C_
5755, 56bitr2i 174 . . . . . . 7  Fun  C_  C_  Fun 
C_  C_  Fun  Fun  C_  C_
5852, 53, 573bitr3i 199 . . . . . 6  Fun  C_  C_  Fun  Fun  C_  C_
59 eluni 3546 . . . . . . . . . 10  <. ,  >.  U.  <. ,  >.
60 eluni 3546 . . . . . . . . . 10  <. ,  >.  U.  <. ,  >.
6159, 60anbi12i 433 . . . . . . . . 9 
<. ,  >. 
U.  <. ,  >.  U.  <. , 
>.  <. , 
>.
62 eeanv 1780 . . . . . . . . 9 
<. ,  >.  <. ,  >.  <. , 
>.  <. , 
>.
63 an4 505 . . . . . . . . . . 11  <. , 
>.  <. ,  >. 
<. ,  >.  <. ,  >.
64 ancom 253 . . . . . . . . . . 11  <. , 
>.  <. ,  >.  <. , 
>.  <. ,  >.
6563, 64bitri 173 . . . . . . . . . 10  <. , 
>.  <. ,  >.  <. , 
>.  <. ,  >.
66652exbii 1470 . . . . . . . . 9 
<. ,  >.  <. ,  >.  <. ,  >.  <. ,  >.
6761, 62, 663bitr2i 197 . . . . . . . 8 
<. ,  >. 
U.  <. ,  >.  U.  <. ,  >.  <. ,  >.
6867imbi1i 227 . . . . . . 7  <. , 
>.  U.  <. ,  >. 
U.  <. ,  >.  <. , 
>.
69 19.23v 1736 . . . . . . 7  <. ,  >.  <. , 
>.  <. ,  >.  <. ,  >.
70 r2al 2312 . . . . . . . 8  <. ,  >.  <. , 
>.  <. ,  >.  <. , 
>.
71 impexp 250 . . . . . . . . 9  <. ,  >.  <. ,  >.  <. ,  >.  <. , 
>.
72712albii 1333 . . . . . . . 8  <. ,  >.  <. , 
>.  <. ,  >.  <. , 
>.
73 19.23v 1736 . . . . . . . . 9  <. ,  >.  <. ,  >.  <. ,  >.  <. ,  >.
7473albii 1332 . . . . . . . 8  <. ,  >.  <. , 
>.  <. ,  >.  <. , 
>.
7570, 72, 743bitr2ri 198 . . . . . . 7  <. ,  >.  <. , 
>.  <. , 
>.  <. ,  >.
7668, 69, 753bitr2i 197 . . . . . 6  <. , 
>.  U.  <. ,  >. 
U.  <. , 
>.  <. ,  >.
7727, 58, 763imtr4i 190 . . . . 5  Fun  C_  C_ 
<. ,  >. 
U.  <. ,  >.  U.
7877alrimiv 1727 . . . 4  Fun  C_  C_  <. , 
>.  U.  <. ,  >. 
U.
7978alrimivv 1728 . . 3  Fun  C_  C_  <. , 
>.  U.  <. ,  >. 
U.
807, 79syl 14 . 2  Fun  C_  C_  <. , 
>.  U.  <. ,  >. 
U.
81 dffun4 4828 . 2  Fun  U.  Rel  U.  <. , 
>.  U.  <. ,  >. 
U.
825, 80, 81sylanbrc 394 1  Fun  C_  C_  Fun  U.
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wo 613  wal 1221  wex 1354   wcel 1366  wral 2275    C_ wss 2885   <.cop 3342   U.cuni 3543   Rel wrel 4265   Fun wfun 4811
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-14 1378  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995  ax-sep 3838  ax-pow 3890  ax-pr 3907
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-eu 1876  df-mo 1877  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ral 2280  df-rex 2281  df-v 2528  df-un 2890  df-in 2892  df-ss 2899  df-pw 3325  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-iun 3622  df-br 3728  df-opab 3782  df-id 3993  df-rel 4267  df-cnv 4268  df-co 4269  df-fun 4819
This theorem is referenced by:  funcnvuni  4882  fun11uni  4883
  Copyright terms: Public domain W3C validator