Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  frrlem4 Structured version   Unicode version

Theorem frrlem4 25577
 Description: Lemma for founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012.)
Hypothesis
Ref Expression
frrlem4.1
Assertion
Ref Expression
frrlem4
Distinct variable groups:   ,,,   ,,,,   ,   ,,,   ,,,   ,,,   ,,   ,,,   ,,,
Allowed substitution hints:   (,,,,)

Proof of Theorem frrlem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frrlem4.1 . . . . . 6
21frrlem2 25575 . . . . 5
3 funfn 5474 . . . . 5
42, 3sylib 189 . . . 4
5 fnresin1 5551 . . . 4
64, 5syl 16 . . 3
8 inss1 3553 . . . . . . . 8
98sseli 3336 . . . . . . 7
101frrlem1 25574 . . . . . . . . 9
1110abeq2i 2542 . . . . . . . 8
12 fndm 5536 . . . . . . . . . 10
13 rsp 2758 . . . . . . . . . . . 12
14133ad2ant3 980 . . . . . . . . . . 11
15 eleq2 2496 . . . . . . . . . . . 12
1615imbi1d 309 . . . . . . . . . . 11
1714, 16syl5ibrcom 214 . . . . . . . . . 10
1812, 17mpan9 456 . . . . . . . . 9
1918exlimiv 1644 . . . . . . . 8
2011, 19sylbi 188 . . . . . . 7
219, 20syl5 30 . . . . . 6
2221imp 419 . . . . 5
2322adantlr 696 . . . 4
24 fvres 5737 . . . . 5
2524adantl 453 . . . 4
26 resres 5151 . . . . . 6
27 predss 25438 . . . . . . . . 9
28 sseqin2 3552 . . . . . . . . 9
2927, 28mpbi 200 . . . . . . . 8
301frrlem1 25574 . . . . . . . . . . . 12
3130abeq2i 2542 . . . . . . . . . . 11
32 eeanv 1937 . . . . . . . . . . . 12
33 simpl1 960 . . . . . . . . . . . . . . . . 17
34 ssinss1 3561 . . . . . . . . . . . . . . . . 17
3533, 34syl 16 . . . . . . . . . . . . . . . 16
36 simpl2 961 . . . . . . . . . . . . . . . . 17
37 simpr2 964 . . . . . . . . . . . . . . . . 17
38 nfra1 2748 . . . . . . . . . . . . . . . . . . 19
39 nfra1 2748 . . . . . . . . . . . . . . . . . . 19
4038, 39nfan 1846 . . . . . . . . . . . . . . . . . 18
41 inss1 3553 . . . . . . . . . . . . . . . . . . . . . 22
4241sseli 3336 . . . . . . . . . . . . . . . . . . . . 21
43 rsp 2758 . . . . . . . . . . . . . . . . . . . . 21
4442, 43syl5com 28 . . . . . . . . . . . . . . . . . . . 20
45 inss2 3554 . . . . . . . . . . . . . . . . . . . . . 22
4645sseli 3336 . . . . . . . . . . . . . . . . . . . . 21
47 rsp 2758 . . . . . . . . . . . . . . . . . . . . 21
4846, 47syl5com 28 . . . . . . . . . . . . . . . . . . . 20
4944, 48anim12d 547 . . . . . . . . . . . . . . . . . . 19
50 ssin 3555 . . . . . . . . . . . . . . . . . . . 20
5150biimpi 187 . . . . . . . . . . . . . . . . . . 19
5249, 51syl6com 33 . . . . . . . . . . . . . . . . . 18
5340, 52ralrimi 2779 . . . . . . . . . . . . . . . . 17
5436, 37, 53syl2anc 643 . . . . . . . . . . . . . . . 16
55 fndm 5536 . . . . . . . . . . . . . . . . . 18
56 ineq12 3529 . . . . . . . . . . . . . . . . . . . 20
5756sseq1d 3367 . . . . . . . . . . . . . . . . . . 19
58 sseq2 3362 . . . . . . . . . . . . . . . . . . . . 21
5958raleqbi1dv 2904 . . . . . . . . . . . . . . . . . . . 20
6056, 59syl 16 . . . . . . . . . . . . . . . . . . 19
6157, 60anbi12d 692 . . . . . . . . . . . . . . . . . 18
6212, 55, 61syl2an 464 . . . . . . . . . . . . . . . . 17
6362biimprcd 217 . . . . . . . . . . . . . . . 16
6435, 54, 63syl2anc 643 . . . . . . . . . . . . . . 15
6564impcom 420 . . . . . . . . . . . . . 14
6665an4s 800 . . . . . . . . . . . . 13
6766exlimivv 1645 . . . . . . . . . . . 12
6832, 67sylbir 205 . . . . . . . . . . 11
6911, 31, 68syl2anb 466 . . . . . . . . . 10
7069adantr 452 . . . . . . . . 9
71 simpr 448 . . . . . . . . 9
72 preddowncl 25463 . . . . . . . . 9
7370, 71, 72sylc 58 . . . . . . . 8
7429, 73syl5eq 2479 . . . . . . 7
7574reseq2d 5138 . . . . . 6
7626, 75syl5eq 2479 . . . . 5
7776oveq2d 6089 . . . 4
7823, 25, 773eqtr4d 2477 . . 3
7978ralrimiva 2781 . 2
807, 79jca 519 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725  cab 2421  wral 2697   cin 3311   wss 3312   cdm 4870   cres 4872   wfun 5440   wfn 5441  cfv 5446  (class class class)co 6073  cpred 25430 This theorem is referenced by:  frrlem5  25578 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-fv 5454  df-ov 6076  df-pred 25431
 Copyright terms: Public domain W3C validator