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

Theorem fununi 4910
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 4862 . . . . 5  Fun  Rel
21adantr 261 . . . 4  Fun  C_  C_ 
Rel
32ralimi 2378 . . 3  Fun  C_  C_  Rel
4 reluni 4403 . . 3  Rel  U.  Rel
53, 4sylibr 137 . 2  Fun  C_  C_  Rel  U.
6 r19.28av 2443 . . . 4  Fun  C_  C_  Fun  C_  C_
76ralimi 2378 . . 3  Fun  C_  C_  Fun  C_  C_
8 ssel 2933 . . . . . . . . . . . . 13 
C_  <. ,  >.  <. ,  >.
98anim1d 319 . . . . . . . . . . . 12 
C_  <. , 
>.  <. ,  >.  <. ,  >.  <. , 
>.
10 dffun4 4856 . . . . . . . . . . . . . . 15  Fun  Rel  <. ,  >.  <. , 
>.
1110simprbi 260 . . . . . . . . . . . . . 14  Fun  <. , 
>.  <. ,  >.
121119.21bbi 1448 . . . . . . . . . . . . 13  Fun  <. , 
>.  <. ,  >.
131219.21bi 1447 . . . . . . . . . . . 12  Fun 
<. ,  >.  <. ,  >.
149, 13syl9r 67 . . . . . . . . . . 11  Fun 
C_  <. , 
>.  <. ,  >.
1514adantl 262 . . . . . . . . . 10  Fun  Fun  C_  <. , 
>.  <. ,  >.
16 ssel 2933 . . . . . . . . . . . . 13 
C_  <. ,  >.  <. ,  >.
1716anim2d 320 . . . . . . . . . . . 12 
C_  <. , 
>.  <. ,  >.  <. ,  >.  <. , 
>.
18 dffun4 4856 . . . . . . . . . . . . . . 15  Fun  Rel  <. ,  >.  <. , 
>.
1918simprbi 260 . . . . . . . . . . . . . 14  Fun 
<. ,  >.  <. ,  >.
201919.21bbi 1448 . . . . . . . . . . . . 13  Fun  <. , 
>.  <. ,  >.
212019.21bi 1447 . . . . . . . . . . . 12  Fun  <. ,  >.  <. , 
>.
2217, 21syl9r 67 . . . . . . . . . . 11  Fun  C_  <. ,  >.  <. , 
>.
2322adantr 261 . . . . . . . . . 10  Fun  Fun  C_  <. , 
>.  <. ,  >.
2415, 23jaod 636 . . . . . . . . 9  Fun  Fun  C_  C_  <. ,  >.  <. , 
>.
2524imp 115 . . . . . . . 8  Fun  Fun  C_  C_  <. , 
>.  <. ,  >.
2625ralimi 2378 . . . . . . 7  Fun  Fun  C_  C_  <. , 
>.  <. ,  >.
2726ralimi 2378 . . . . . 6  Fun  Fun  C_  C_  <. ,  >.  <. , 
>.
28 funeq 4864 . . . . . . . . . 10  Fun  Fun
29 sseq1 2960 . . . . . . . . . . 11  C_  C_
30 sseq2 2961 . . . . . . . . . . 11  C_  C_
3129, 30orbi12d 706 . . . . . . . . . 10  C_  C_  C_  C_
3228, 31anbi12d 442 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
33 sseq2 2961 . . . . . . . . . . 11  C_  C_
34 sseq1 2960 . . . . . . . . . . 11  C_  C_
3533, 34orbi12d 706 . . . . . . . . . 10  C_  C_  C_  C_
3635anbi2d 437 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
3732, 36cbvral2v 2535 . . . . . . . 8  Fun  C_  C_  Fun  C_  C_
38 ralcom 2467 . . . . . . . . 9  Fun  C_  C_  Fun  C_  C_
39 orcom 646 . . . . . . . . . . . 12  C_  C_ 
C_  C_
40 sseq1 2960 . . . . . . . . . . . . 13  C_  C_
41 sseq2 2961 . . . . . . . . . . . . 13  C_  C_
4240, 41orbi12d 706 . . . . . . . . . . . 12  C_  C_  C_  C_
4339, 42syl5bb 181 . . . . . . . . . . 11  C_  C_  C_  C_
4443anbi2d 437 . . . . . . . . . 10  Fun  C_  C_  Fun 
C_  C_
45 funeq 4864 . . . . . . . . . . 11  Fun  Fun
46 sseq2 2961 . . . . . . . . . . . 12  C_  C_
47 sseq1 2960 . . . . . . . . . . . 12  C_  C_
4846, 47orbi12d 706 . . . . . . . . . . 11  C_  C_  C_  C_
4945, 48anbi12d 442 . . . . . . . . . 10  Fun  C_  C_  Fun 
C_  C_
5044, 49cbvral2v 2535 . . . . . . . . 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 525 . . . . . . . . 9  Fun  Fun  C_  C_  Fun  C_  C_  Fun  C_  C_
55542ralbii 2326 . . . . . . . 8  Fun  Fun  C_  C_  Fun  C_  C_  Fun 
C_  C_
56 r19.26-2 2436 . . . . . . . 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 3574 . . . . . . . . . 10  <. ,  >.  U.  <. ,  >.
60 eluni 3574 . . . . . . . . . 10  <. ,  >.  U.  <. ,  >.
6159, 60anbi12i 433 . . . . . . . . 9 
<. ,  >. 
U.  <. ,  >.  U.  <. , 
>.  <. , 
>.
62 eeanv 1804 . . . . . . . . 9 
<. ,  >.  <. ,  >.  <. , 
>.  <. , 
>.
63 an4 520 . . . . . . . . . . 11  <. , 
>.  <. ,  >. 
<. ,  >.  <. ,  >.
64 ancom 253 . . . . . . . . . . 11  <. , 
>.  <. ,  >.  <. , 
>.  <. ,  >.
6563, 64bitri 173 . . . . . . . . . 10  <. , 
>.  <. ,  >.  <. , 
>.  <. ,  >.
66652exbii 1494 . . . . . . . . 9 
<. ,  >.  <. ,  >.  <. ,  >.  <. ,  >.
6761, 62, 663bitr2i 197 . . . . . . . 8 
<. ,  >. 
U.  <. ,  >.  U.  <. ,  >.  <. ,  >.
6867imbi1i 227 . . . . . . 7  <. , 
>.  U.  <. ,  >. 
U.  <. ,  >.  <. , 
>.
69 19.23v 1760 . . . . . . 7  <. ,  >.  <. , 
>.  <. ,  >.  <. ,  >.
70 r2al 2337 . . . . . . . 8  <. ,  >.  <. , 
>.  <. ,  >.  <. , 
>.
71 impexp 250 . . . . . . . . 9  <. ,  >.  <. ,  >.  <. ,  >.  <. , 
>.
72712albii 1357 . . . . . . . 8  <. ,  >.  <. , 
>.  <. ,  >.  <. , 
>.
73 19.23v 1760 . . . . . . . . 9  <. ,  >.  <. ,  >.  <. ,  >.  <. ,  >.
7473albii 1356 . . . . . . . 8  <. ,  >.  <. , 
>.  <. ,  >.  <. , 
>.
7570, 72, 743bitr2ri 198 . . . . . . 7  <. ,  >.  <. , 
>.  <. , 
>.  <. ,  >.
7668, 69, 753bitr2i 197 . . . . . 6  <. , 
>.  U.  <. ,  >. 
U.  <. , 
>.  <. ,  >.
7727, 58, 763imtr4i 190 . . . . 5  Fun  C_  C_ 
<. ,  >. 
U.  <. ,  >.  U.
7877alrimiv 1751 . . . 4  Fun  C_  C_  <. , 
>.  U.  <. ,  >. 
U.
7978alrimivv 1752 . . 3  Fun  C_  C_  <. , 
>.  U.  <. ,  >. 
U.
807, 79syl 14 . 2  Fun  C_  C_  <. , 
>.  U.  <. ,  >. 
U.
81 dffun4 4856 . 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 628  wal 1240  wex 1378   wcel 1390  wral 2300    C_ wss 2911   <.cop 3370   U.cuni 3571   Rel wrel 4293   Fun wfun 4839
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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-iun 3650  df-br 3756  df-opab 3810  df-id 4021  df-rel 4295  df-cnv 4296  df-co 4297  df-fun 4847
This theorem is referenced by:  funcnvuni  4911  fun11uni  4912
  Copyright terms: Public domain W3C validator