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

Theorem fun11iun 5090
Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by Mario Carneiro, 20-May-2013.) (Revised by Mario Carneiro, 24-Jun-2015.)
Hypotheses
Ref Expression
fun11iun.1  C
fun11iun.2  _V
Assertion
Ref Expression
fun11iun  : D -1-1-> S  C_  C  C  C_  U_  : U_  D -1-1-> S
Distinct variable groups:   ,   ,   ,   , C   , S
Allowed substitution hints:   ()    C()    D(,)    S()

Proof of Theorem fun11iun
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2554 . . . . . . . . . 10 
_V
2 eqeq1 2043 . . . . . . . . . . 11
32rexbidv 2321 . . . . . . . . . 10
41, 3elab 2681 . . . . . . . . 9  {  |  }
5 r19.29 2444 . . . . . . . . . 10  : D -1-1-> S  C_  C  C  C_  : D -1-1-> S  C_  C  C  C_
6 nfv 1418 . . . . . . . . . . . 12  F/ Fun  Fun  `'
7 nfre1 2359 . . . . . . . . . . . . . 14  F/
87nfab 2179 . . . . . . . . . . . . 13  F/_ {  |  }
9 nfv 1418 . . . . . . . . . . . . 13  F/  C_  C_
108, 9nfralxy 2354 . . . . . . . . . . . 12  F/  {  |  }  C_  C_
116, 10nfan 1454 . . . . . . . . . . 11  F/ Fun  Fun  `'  {  |  }  C_  C_
12 f1eq1 5030 . . . . . . . . . . . . . . . 16  : D -1-1-> S  : D -1-1-> S
1312biimparc 283 . . . . . . . . . . . . . . 15  : D -1-1-> S  : D -1-1-> S
14 df-f1 4850 . . . . . . . . . . . . . . . 16  : D -1-1-> S  : D --> S  Fun  `'
15 ffun 4991 . . . . . . . . . . . . . . . . 17  : D --> S 
Fun
1615anim1i 323 . . . . . . . . . . . . . . . 16  : D --> S  Fun  `'  Fun  Fun  `'
1714, 16sylbi 114 . . . . . . . . . . . . . . 15  : D -1-1-> S  Fun  Fun  `'
1813, 17syl 14 . . . . . . . . . . . . . 14  : D -1-1-> S  Fun  Fun  `'
1918adantlr 446 . . . . . . . . . . . . 13  : D -1-1-> S  C_  C  C  C_  Fun  Fun  `'
20 vex 2554 . . . . . . . . . . . . . . . 16 
_V
21 eqeq1 2043 . . . . . . . . . . . . . . . . 17
2221rexbidv 2321 . . . . . . . . . . . . . . . 16
2320, 22elab 2681 . . . . . . . . . . . . . . 15  {  |  }
24 fun11iun.1 . . . . . . . . . . . . . . . . . 18  C
2524eqeq2d 2048 . . . . . . . . . . . . . . . . 17  C
2625cbvrexv 2528 . . . . . . . . . . . . . . . 16  C
27 r19.29 2444 . . . . . . . . . . . . . . . . . . 19  C_  C  C  C_  C  C_  C  C  C_  C
28 sseq12 2962 . . . . . . . . . . . . . . . . . . . . . . . . 25  C  C_  C_  C
2928ancoms 255 . . . . . . . . . . . . . . . . . . . . . . . 24  C  C_  C_  C
30 sseq12 2962 . . . . . . . . . . . . . . . . . . . . . . . 24  C  C_  C  C_
3129, 30orbi12d 706 . . . . . . . . . . . . . . . . . . . . . . 23  C  C_  C_  C_  C  C  C_
3231biimprcd 149 . . . . . . . . . . . . . . . . . . . . . 22  C_  C  C  C_  C  C_  C_
3332expdimp 246 . . . . . . . . . . . . . . . . . . . . 21  C_  C  C  C_  C 
C_  C_
3433rexlimivw 2423 . . . . . . . . . . . . . . . . . . . 20  C_  C  C  C_  C  C_  C_
3534imp 115 . . . . . . . . . . . . . . . . . . 19  C_  C  C  C_  C  C_  C_
3627, 35sylan 267 . . . . . . . . . . . . . . . . . 18  C_  C  C  C_  C  C_  C_
3736an32s 502 . . . . . . . . . . . . . . . . 17  C_  C  C  C_  C  C_  C_
3837adantlll 449 . . . . . . . . . . . . . . . 16  : D -1-1-> S  C_  C  C  C_  C  C_  C_
3926, 38sylan2b 271 . . . . . . . . . . . . . . 15  : D -1-1-> S  C_  C  C  C_  C_  C_
4023, 39sylan2b 271 . . . . . . . . . . . . . 14  : D -1-1-> S  C_  C  C  C_  {  |  }  C_  C_
4140ralrimiva 2386 . . . . . . . . . . . . 13  : D -1-1-> S  C_  C  C  C_ 
{  |  } 
C_  C_
4219, 41jca 290 . . . . . . . . . . . 12  : D -1-1-> S  C_  C  C  C_  Fun  Fun  `' 
{  |  } 
C_  C_
4342a1i 9 . . . . . . . . . . 11  : D -1-1-> S  C_  C  C  C_  Fun  Fun  `' 
{  |  } 
C_  C_
4411, 43rexlimi 2420 . . . . . . . . . 10  : D -1-1-> S  C_  C  C  C_  Fun  Fun  `' 
{  |  } 
C_  C_
455, 44syl 14 . . . . . . . . 9  : D -1-1-> S  C_  C  C  C_  Fun  Fun  `'  {  |  }  C_  C_
464, 45sylan2b 271 . . . . . . . 8  : D -1-1-> S  C_  C  C  C_  {  |  }  Fun  Fun  `'  {  |  }  C_  C_
4746ralrimiva 2386 . . . . . . 7  : D -1-1-> S  C_  C  C  C_  {  |  }  Fun  Fun  `'  {  |  }  C_  C_
48 fun11uni 4912 . . . . . . 7  {  |  }  Fun  Fun  `'  {  |  }  C_  C_  Fun  U. {  |  }  Fun  `'
U. {  |  }
4947, 48syl 14 . . . . . 6  : D -1-1-> S  C_  C  C  C_  Fun  U. {  |  }  Fun  `' U. {  |  }
5049simpld 105 . . . . 5  : D -1-1-> S  C_  C  C  C_  Fun  U. {  |  }
51 fun11iun.2 . . . . . . 7  _V
5251dfiun2 3682 . . . . . 6  U_  U. {  |  }
5352funeqi 4865 . . . . 5  Fun  U_  Fun  U. {  |  }
5450, 53sylibr 137 . . . 4  : D -1-1-> S  C_  C  C  C_  Fun  U_
55 nfra1 2349 . . . . . . 7  F/  : D -1-1-> S  C_  C  C  C_
56 rsp 2363 . . . . . . . . 9  : D -1-1-> S  C_  C  C  C_  : D -1-1-> S  C_  C  C  C_
571eldm2 4476 . . . . . . . . . . 11  dom  <. ,  >.
58 f1dm 5039 . . . . . . . . . . . 12  : D -1-1-> S 
dom  D
5958eleq2d 2104 . . . . . . . . . . 11  : D -1-1-> S  dom  D
6057, 59syl5bbr 183 . . . . . . . . . 10  : D -1-1-> S  <. ,  >.  D
6160adantr 261 . . . . . . . . 9  : D -1-1-> S  C_  C  C  C_  <. ,  >.  D
6256, 61syl6 29 . . . . . . . 8  : D -1-1-> S  C_  C  C  C_  <. ,  >.  D
6362imp 115 . . . . . . 7  : D -1-1-> S  C_  C  C  C_  <. ,  >.  D
6455, 63rexbida 2315 . . . . . 6  : D -1-1-> S  C_  C  C  C_  <. ,  >.  D
65 eliun 3652 . . . . . . . 8  <. ,  >.  U_  <. ,  >.
6665exbii 1493 . . . . . . 7  <. , 
>.  U_  <. ,  >.
671eldm2 4476 . . . . . . 7  dom  U_  <. ,  >. 
U_
68 rexcom4 2571 . . . . . . 7  <. ,  >.  <. ,  >.
6966, 67, 683bitr4i 201 . . . . . 6  dom  U_  <. ,  >.
70 eliun 3652 . . . . . 6  U_  D  D
7164, 69, 703bitr4g 212 . . . . 5  : D -1-1-> S  C_  C  C  C_  dom  U_  U_  D
7271eqrdv 2035 . . . 4  : D -1-1-> S  C_  C  C  C_  dom  U_  U_  D
73 df-fn 4848 . . . 4  U_  Fn  U_  D  Fun  U_  dom  U_  U_  D
7454, 72, 73sylanbrc 394 . . 3  : D -1-1-> S  C_  C  C  C_  U_  Fn  U_  D
75 rniun 4677 . . . 4  ran  U_  U_  ran
76 f1f 5035 . . . . . . . 8  : D -1-1-> S  : D --> S
77 frn 4995 . . . . . . . 8  : D --> S 
ran  C_  S
7876, 77syl 14 . . . . . . 7  : D -1-1-> S 
ran  C_  S
7978adantr 261 . . . . . 6  : D -1-1-> S  C_  C  C  C_  ran  C_  S
8079ralimi 2378 . . . . 5  : D -1-1-> S  C_  C  C  C_  ran  C_  S
81 iunss 3689 . . . . 5  U_  ran 
C_  S  ran  C_  S
8280, 81sylibr 137 . . . 4  : D -1-1-> S  C_  C  C  C_  U_  ran  C_  S
8375, 82syl5eqss 2983 . . 3  : D -1-1-> S  C_  C  C  C_  ran  U_  C_  S
84 df-f 4849 . . 3  U_  : U_  D
--> S  U_  Fn  U_  D  ran  U_  C_  S
8574, 83, 84sylanbrc 394 . 2  : D -1-1-> S  C_  C  C  C_  U_  : U_  D --> S
8649simprd 107 . . 3  : D -1-1-> S  C_  C  C  C_  Fun  `' U. {  |  }
8752cnveqi 4453 . . . 4  `' U_  `' U. {  |  }
8887funeqi 4865 . . 3  Fun  `' U_  Fun  `' U. {  |  }
8986, 88sylibr 137 . 2  : D -1-1-> S  C_  C  C  C_  Fun  `' U_
90 df-f1 4850 . 2  U_  : U_  D -1-1-> S  U_  : U_  D
--> S  Fun  `' U_
9185, 89, 90sylanbrc 394 1  : D -1-1-> S  C_  C  C  C_  U_  : U_  D -1-1-> S
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   wo 628   wceq 1242  wex 1378   wcel 1390   {cab 2023  wral 2300  wrex 2301   _Vcvv 2551    C_ wss 2911   <.cop 3370   U.cuni 3571   U_ciun 3648   `'ccnv 4287   dom cdm 4288   ran crn 4289   Fun wfun 4839    Fn wfn 4840   -->wf 4841   -1-1->wf1 4842
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-bnd 1396  ax-4 1397  ax-13 1401  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  ax-un 4136
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-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator