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

Theorem tfrlem9 5876
Description: Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
Hypothesis
Ref Expression
tfrlem.1  {  |  On  Fn  `  F `  |`  }
Assertion
Ref Expression
tfrlem9  dom recs F recs F `  F ` recs F  |`
Distinct variable groups:   ,,,   , F,,
Allowed substitution hints:   (,,)

Proof of Theorem tfrlem9
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eldm2g 4474 . . 3  dom recs F  dom recs F  <. ,  >. recs F
21ibi 165 . 2  dom recs F  <. ,  >. recs F
3 df-recs 5861 . . . . . 6 recs F  U. {  |  On  Fn  `  F `  |`  }
43eleq2i 2101 . . . . 5  <. ,  >. recs F  <. ,  >.  U. {  |  On  Fn  `  F `  |`  }
5 eluniab 3583 . . . . 5  <. ,  >.  U. {  |  On  Fn  `  F `  |`  }  <. , 
>.  On  Fn  `  F `  |`
64, 5bitri 173 . . . 4  <. ,  >. recs F  <. , 
>.  On  Fn  `  F `  |`
7 fnop 4945 . . . . . . . . . . . . . 14  Fn  <. ,  >.
8 rspe 2364 . . . . . . . . . . . . . . . 16  On  Fn  `  F `  |`  On  Fn  `  F `  |`
9 tfrlem.1 . . . . . . . . . . . . . . . . . 18  {  |  On  Fn  `  F `  |`  }
109abeq2i 2145 . . . . . . . . . . . . . . . . 17  On  Fn  `  F `  |`
11 elssuni 3599 . . . . . . . . . . . . . . . . . 18  C_ 
U.
129recsfval 5872 . . . . . . . . . . . . . . . . . 18 recs F  U.
1311, 12syl6sseqr 2986 . . . . . . . . . . . . . . . . 17  C_ recs F
1410, 13sylbir 125 . . . . . . . . . . . . . . . 16  On  Fn  `  F `  |`  C_ recs F
158, 14syl 14 . . . . . . . . . . . . . . 15  On  Fn  `  F `  |`  C_ recs F
16 fveq2 5121 . . . . . . . . . . . . . . . . . . . 20  `  `
17 reseq2 4550 . . . . . . . . . . . . . . . . . . . . 21  |`  |`
1817fveq2d 5125 . . . . . . . . . . . . . . . . . . . 20  F `  |`  F `  |`
1916, 18eqeq12d 2051 . . . . . . . . . . . . . . . . . . 19  `  F `  |`  `  F `  |`
2019rspcv 2646 . . . . . . . . . . . . . . . . . 18  `  F `  |`  `
 F `  |`
21 fndm 4941 . . . . . . . . . . . . . . . . . . . . 21  Fn  dom
2221eleq2d 2104 . . . . . . . . . . . . . . . . . . . 20  Fn  dom
239tfrlem7 5874 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  Fun recs F
24 funssfv 5142 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  Fun recs F  C_ recs F  dom recs F `  `
2523, 24mp3an1 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  C_ recs F  dom recs F `  `
2625adantrl 447 . . . . . . . . . . . . . . . . . . . . . . . . . 26  C_ recs F  Fn  On  dom recs F `
 `
2721eleq1d 2103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  Fn  dom  On  On
28 onelss 4090 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  dom  On  dom  C_  dom
2927, 28syl6bir 153 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  Fn  On  dom  C_  dom
3029imp31 243 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  Fn  On  dom  C_  dom
31 fun2ssres 4886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  Fun recs F  C_ recs F  C_  dom recs F  |`  |`
3231fveq2d 5125 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  Fun recs F  C_ recs F  C_  dom  F ` recs F  |`  F `
 |`
3323, 32mp3an1 1218 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  C_ recs F  C_  dom  F ` recs F  |`  F `
 |`
3430, 33sylan2 270 . . . . . . . . . . . . . . . . . . . . . . . . . 26  C_ recs F  Fn  On  dom  F ` recs F  |`  F `
 |`
3526, 34eqeq12d 2051 . . . . . . . . . . . . . . . . . . . . . . . . 25  C_ recs F  Fn  On  dom recs F `  F ` recs F  |`  `
 F `  |`
3635exbiri 364 . . . . . . . . . . . . . . . . . . . . . . . 24 
C_ recs F  Fn  On  dom  `  F `  |` recs F `  F ` recs F  |`
3736com3l 75 . . . . . . . . . . . . . . . . . . . . . . 23  Fn  On  dom  `  F `  |` 
C_ recs F recs F `  F ` recs F  |`
3837exp31 346 . . . . . . . . . . . . . . . . . . . . . 22  Fn  On  dom  `
 F `  |`  C_ recs F recs F `  F ` recs F  |`
3938com34 77 . . . . . . . . . . . . . . . . . . . . 21  Fn  On  `  F `  |`  dom  C_ recs F recs F `  F ` recs F  |`
4039com24 81 . . . . . . . . . . . . . . . . . . . 20  Fn  dom  `  F `  |`  On  C_ recs F recs F `
 F ` recs F  |`
4122, 40sylbird 159 . . . . . . . . . . . . . . . . . . 19  Fn  `  F `  |`  On  C_ recs F recs F `
 F ` recs F  |`
4241com3l 75 . . . . . . . . . . . . . . . . . 18  `  F `  |`  Fn  On  C_ recs F recs F `  F ` recs F  |`
4320, 42syld 40 . . . . . . . . . . . . . . . . 17  `  F `  |`  Fn  On  C_ recs F recs F `  F ` recs F  |`
4443com24 81 . . . . . . . . . . . . . . . 16  On  Fn  `  F `  |`  C_ recs F recs F `  F ` recs F  |`
4544imp4d 334 . . . . . . . . . . . . . . 15  On  Fn  `  F `  |`  C_ recs F recs F `  F ` recs F  |`
4615, 45mpdi 38 . . . . . . . . . . . . . 14  On  Fn  `  F `  |` recs F `  F ` recs F  |`
477, 46syl 14 . . . . . . . . . . . . 13  Fn  <. ,  >.  On  Fn  `  F `  |` recs F `  F ` recs F  |`
4847exp4d 351 . . . . . . . . . . . 12  Fn  <. ,  >.  On  Fn  `  F `  |` recs F `  F ` recs F  |`
4948ex 108 . . . . . . . . . . 11  Fn  <. ,  >.  On  Fn  `  F `  |` recs F `  F ` recs F  |`
5049com4r 80 . . . . . . . . . 10  Fn  Fn  <. ,  >.  On  `  F `  |` recs F `  F ` recs F  |`
5150pm2.43i 43 . . . . . . . . 9  Fn  <. ,  >.  On  `  F `  |` recs F `  F ` recs F  |`
5251com3l 75 . . . . . . . 8  <. ,  >.  On  Fn  `  F `  |` recs F `  F ` recs F  |`
5352imp4a 331 . . . . . . 7  <. ,  >.  On  Fn  `  F `  |` recs F `
 F ` recs F  |`
5453rexlimdv 2426 . . . . . 6  <. ,  >.  On  Fn  `  F `  |` recs F `
 F ` recs F  |`
5554imp 115 . . . . 5 
<. ,  >.  On  Fn  `  F `  |` recs F `  F ` recs F  |`
5655exlimiv 1486 . . . 4  <. , 
>.  On  Fn  `  F `  |` recs F `  F ` recs F  |`
576, 56sylbi 114 . . 3  <. ,  >. recs F recs F `  F ` recs F  |`
5857exlimiv 1486 . 2  <. , 
>. recs F recs F `
 F ` recs F  |`
592, 58syl 14 1  dom recs F recs F `  F ` recs F  |`
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   w3a 884   wceq 1242  wex 1378   wcel 1390   {cab 2023  wral 2300  wrex 2301    C_ wss 2911   <.cop 3370   U.cuni 3571   Oncon0 4066   dom cdm 4288    |` cres 4290   Fun wfun 4839    Fn wfn 4840   ` cfv 4845  recscrecs 5860
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-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-setind 4220
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-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  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-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853  df-recs 5861
This theorem is referenced by:  tfr2a  5877  tfrlemiubacc  5885
  Copyright terms: Public domain W3C validator