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

Theorem wfrlem5 29543
 Description: Lemma for well-founded recursion. The values of two acceptable functions agree within their domains. (Contributed by Scott Fenton, 21-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.)
Hypotheses
Ref Expression
wfrlem5.1
wfrlem5.2 Se
wfrlem5.3
Assertion
Ref Expression
wfrlem5
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,
Allowed substitution hints:   (,)   (,,,,,,)   (,)   (,)

Proof of Theorem wfrlem5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 3112 . . . . . 6
2 vex 3112 . . . . . 6
31, 2breldm 5217 . . . . 5
4 vex 3112 . . . . . 6
51, 4breldm 5217 . . . . 5
63, 5anim12i 566 . . . 4
7 elin 3683 . . . 4
86, 7sylibr 212 . . 3
9 anandir 829 . . . . 5
102brres 5290 . . . . . 6
114brres 5290 . . . . . 6
1210, 11anbi12i 697 . . . . 5
139, 12bitr4i 252 . . . 4
1413biimpi 194 . . 3
158, 14mpdan 668 . 2
16 wfrlem5.3 . . . . . . . . 9
1716wfrlem3 29541 . . . . . . . 8
18 ssinss1 3722 . . . . . . . 8
19 wfrlem5.1 . . . . . . . . . 10
20 wess 4875 . . . . . . . . . 10
2119, 20mpi 17 . . . . . . . . 9
22 wfrlem5.2 . . . . . . . . . 10 Se
23 sess2 4857 . . . . . . . . . 10 Se Se
2422, 23mpi 17 . . . . . . . . 9 Se
2521, 24jca 532 . . . . . . . 8 Se
2617, 18, 253syl 20 . . . . . . 7 Se
2726adantr 465 . . . . . 6 Se
2819, 16wfrlem4 29542 . . . . . 6
2919, 16wfrlem4 29542 . . . . . . . 8
3029ancoms 453 . . . . . . 7
31 incom 3687 . . . . . . . . . . 11
3231reseq2i 5280 . . . . . . . . . 10
3332fneq1i 5681 . . . . . . . . 9
3431fneq2i 5682 . . . . . . . . 9
3533, 34bitri 249 . . . . . . . 8
3632fveq1i 5873 . . . . . . . . . 10
37 predeq2 29443 . . . . . . . . . . . . 13
3831, 37ax-mp 5 . . . . . . . . . . . 12
3932, 38reseq12i 5281 . . . . . . . . . . 11
4039fveq2i 5875 . . . . . . . . . 10
4136, 40eqeq12i 2477 . . . . . . . . 9
4231, 41raleqbii 2902 . . . . . . . 8
4335, 42anbi12i 697 . . . . . . 7
4430, 43sylibr 212 . . . . . 6
45 wfr3g 29538 . . . . . 6 Se
4627, 28, 44, 45syl3anc 1228 . . . . 5
4746breqd 4467 . . . 4
4847biimprd 223 . . 3
4916wfrlem2 29540 . . . . 5
50 funres 5633 . . . . 5
51 dffun2 5604 . . . . . 6
5251simprbi 464 . . . . 5
53 2sp 1867 . . . . . 6
5453sps 1866 . . . . 5
5549, 50, 52, 544syl 21 . . . 4