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

Theorem tfrlemisucaccv 5880
Description: We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5887. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
Hypotheses
Ref Expression
tfrlemisucfn.1  {  |  On  Fn  `  F `  |`  }
tfrlemisucfn.2  Fun 
F  F `  _V
tfrlemisucfn.3  On
tfrlemisucfn.4  Fn
tfrlemisucfn.5
Assertion
Ref Expression
tfrlemisucaccv  u.  { <. ,  F `
 >. }
Distinct variable groups:   ,,,,,   , F,,,,   ,
Allowed substitution hints:   (,,,)

Proof of Theorem tfrlemisucaccv
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlemisucfn.3 . . . 4  On
2 suceloni 4193 . . . 4  On  suc  On
31, 2syl 14 . . 3  suc  On
4 tfrlemisucfn.1 . . . 4  {  |  On  Fn  `  F `  |`  }
5 tfrlemisucfn.2 . . . 4  Fun 
F  F `  _V
6 tfrlemisucfn.4 . . . 4  Fn
7 tfrlemisucfn.5 . . . 4
84, 5, 1, 6, 7tfrlemisucfn 5879 . . 3  u.  { <. ,  F `
 >. }  Fn  suc
9 vex 2554 . . . . . 6 
_V
109elsuc 4109 . . . . 5  suc
11 vex 2554 . . . . . . . . . . 11 
_V
124, 11tfrlem3a 5866 . . . . . . . . . 10  On  Fn  `  F `  |`
137, 12sylib 127 . . . . . . . . 9  On  Fn  `  F `  |`
14 simprrr 492 . . . . . . . . . 10  On  Fn  `  F `  |`  `  F `  |`
15 simprrl 491 . . . . . . . . . . . 12  On  Fn  `  F `  |`  Fn
166adantr 261 . . . . . . . . . . . 12  On  Fn  `  F `  |`  Fn
17 fndmu 4943 . . . . . . . . . . . 12  Fn  Fn
1815, 16, 17syl2anc 391 . . . . . . . . . . 11  On  Fn  `  F `  |`
1918raleqdv 2505 . . . . . . . . . 10  On  Fn  `  F `  |`  `  F `  |`  `  F `  |`
2014, 19mpbid 135 . . . . . . . . 9  On  Fn  `  F `  |`  `  F `  |`
2113, 20rexlimddv 2431 . . . . . . . 8  `  F `  |`
2221r19.21bi 2401 . . . . . . 7  `
 F `  |`
23 elirrv 4226 . . . . . . . . . . 11
24 elequ2 1598 . . . . . . . . . . 11
2523, 24mtbiri 599 . . . . . . . . . 10
2625necon2ai 2253 . . . . . . . . 9  =/=
2726adantl 262 . . . . . . . 8  =/=
28 fvunsng 5300 . . . . . . . 8  _V  =/=  u.  { <. ,  F `
 >. } `  `
299, 27, 28sylancr 393 . . . . . . 7  u.  { <. ,  F `  >. } `  `
30 eloni 4078 . . . . . . . . . . . 12  On  Ord
311, 30syl 14 . . . . . . . . . . 11  Ord
32 ordelss 4082 . . . . . . . . . . 11  Ord  C_
3331, 32sylan 267 . . . . . . . . . 10  C_
34 resabs1 4583 . . . . . . . . . 10 
C_  u.  { <. ,  F `
 >. }  |`  |`  u.  { <. ,  F `
 >. }  |`
3533, 34syl 14 . . . . . . . . 9  u.  { <. ,  F `
 >. }  |`  |`  u.  { <. ,  F `
 >. }  |`
36 elirrv 4226 . . . . . . . . . . . 12
37 fsnunres 5307 . . . . . . . . . . . 12  Fn  u.  { <. ,  F `  >. }  |`
386, 36, 37sylancl 392 . . . . . . . . . . 11  u. 
{ <. ,  F ` 
>. }  |`
3938reseq1d 4554 . . . . . . . . . 10  u.  { <. ,  F `  >. }  |`  |`  |`
4039adantr 261 . . . . . . . . 9  u.  { <. ,  F `
 >. }  |`  |`  |`
4135, 40eqtr3d 2071 . . . . . . . 8  u.  { <. ,  F `  >. }  |`  |`
4241fveq2d 5125 . . . . . . 7  F `
 u.  { <. ,  F `  >. }  |`  F `  |`
4322, 29, 423eqtr4d 2079 . . . . . 6  u.  { <. ,  F `  >. } `  F `  u.  { <. ,  F `  >. }  |`
445tfrlem3-2d 5869 . . . . . . . . . 10  Fun  F  F `  _V
4544simprd 107 . . . . . . . . 9  F `  _V
46 fndm 4941 . . . . . . . . . . . 12  Fn  dom
476, 46syl 14 . . . . . . . . . . 11  dom
4847eleq2d 2104 . . . . . . . . . 10  dom
4936, 48mtbiri 599 . . . . . . . . 9  dom
50 fsnunfv 5306 . . . . . . . . 9  On  F `  _V  dom  u. 
{ <. ,  F ` 
>. } `  F `
511, 45, 49, 50syl3anc 1134 . . . . . . . 8  u. 
{ <. ,  F ` 
>. } `  F `
5251adantr 261 . . . . . . 7  u.  { <. ,  F `  >. } `  F `
53 simpr 103 . . . . . . . 8
5453fveq2d 5125 . . . . . . 7  u.  { <. ,  F `  >. } `  u.  { <. ,  F `  >. } `
55 reseq2 4550 . . . . . . . . 9  u.  { <. ,  F `  >. }  |`  u.  { <. ,  F `  >. }  |`
5655, 38sylan9eqr 2091 . . . . . . . 8  u.  { <. ,  F `  >. }  |`
5756fveq2d 5125 . . . . . . 7  F `
 u.  { <. ,  F `  >. }  |`  F `
5852, 54, 573eqtr4d 2079 . . . . . 6  u.  { <. ,  F `  >. } `  F `  u.  { <. ,  F `  >. }  |`
5943, 58jaodan 709 . . . . 5  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`
6010, 59sylan2b 271 . . . 4  suc  u.  { <. ,  F `  >. } `  F `  u.  { <. ,  F `  >. }  |`
6160ralrimiva 2386 . . 3  suc  u. 
{ <. ,  F ` 
>. } `  F `  u. 
{ <. ,  F ` 
>. }  |`
62 fneq2 4931 . . . . 5  suc  u.  { <. ,  F `
 >. }  Fn  u.  { <. ,  F `  >. }  Fn 
suc
63 raleq 2499 . . . . 5  suc  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`  suc  u. 
{ <. ,  F ` 
>. } `  F `  u. 
{ <. ,  F ` 
>. }  |`
6462, 63anbi12d 442 . . . 4  suc  u. 
{ <. ,  F ` 
>. }  Fn  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`  u.  { <. ,  F `  >. }  Fn 
suc  suc  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`
6564rspcev 2650 . . 3  suc  On  u. 
{ <. ,  F ` 
>. }  Fn  suc 
suc  u.  { <. ,  F `  >. } `  F `  u.  { <. ,  F `  >. }  |`  On  u.  { <. ,  F `
 >. }  Fn  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`
663, 8, 61, 65syl12anc 1132 . 2  On  u.  { <. ,  F `
 >. }  Fn  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`
67 vex 2554 . . . . . 6 
_V
68 opexg 3955 . . . . . 6  _V  F `  _V  <. ,  F `
 >. 
_V
6967, 45, 68sylancr 393 . . . . 5  <. ,  F ` 
>.  _V
70 snexg 3927 . . . . 5  <. ,  F `  >.  _V  { <. ,  F ` 
>. }  _V
7169, 70syl 14 . . . 4  { <. ,  F ` 
>. }  _V
72 unexg 4144 . . . 4  _V  {
<. ,  F `
 >. }  _V  u.  { <. ,  F `  >. } 
_V
7311, 71, 72sylancr 393 . . 3  u.  { <. ,  F `
 >. }  _V
744tfrlem3ag 5865 . . 3  u.  { <. ,  F `  >. } 
_V  u.  { <. ,  F `  >. }  On  u.  { <. ,  F `  >. }  Fn  u.  { <. ,  F `  >. } `  F `  u.  { <. ,  F `  >. }  |`
7573, 74syl 14 . 2  u. 
{ <. ,  F ` 
>. }  On  u.  { <. ,  F `
 >. }  Fn  u.  { <. ,  F `
 >. } `  F `  u.  { <. ,  F `
 >. }  |`
7666, 75mpbird 156 1  u.  { <. ,  F `
 >. }
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 97   wb 98   wo 628  wal 1240   wceq 1242   wcel 1390   {cab 2023    =/= wne 2201  wral 2300  wrex 2301   _Vcvv 2551    u. cun 2909    C_ wss 2911   {csn 3367   <.cop 3370   Ord word 4065   Oncon0 4066   suc csuc 4068   dom cdm 4288    |` cres 4290   Fun wfun 4839    Fn wfn 4840   ` cfv 4845
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-in1 544  ax-in2 545  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-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  ax-setind 4220
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-fal 1248  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-ne 2203  df-ral 2305  df-rex 2306  df-v 2553  df-sbc 2759  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-suc 4074  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
This theorem is referenced by:  tfrlemibacc  5881  tfrlemi14d  5888
  Copyright terms: Public domain W3C validator