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

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

Proof of Theorem frrlem5
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 vex 2951 . . . . . 6
2 vex 2951 . . . . . 6
31, 2breldm 5066 . . . . 5
4 vex 2951 . . . . . 6
51, 4breldm 5066 . . . . 5
63, 5anim12i 550 . . . 4
7 elin 3522 . . . 4
86, 7sylibr 204 . . 3
9 anandir 803 . . . . 5
102brres 5144 . . . . . 6
114brres 5144 . . . . . 6
1210, 11anbi12i 679 . . . . 5
139, 12bitr4i 244 . . . 4
1413biimpi 187 . . 3
158, 14mpdan 650 . 2
16 frrlem5.3 . . . . . . . . 9
1716frrlem3 25576 . . . . . . . 8
18 ssinss1 3561 . . . . . . . 8
19 frrlem5.1 . . . . . . . . . 10
20 frss 4541 . . . . . . . . . 10
2119, 20mpi 17 . . . . . . . . 9
22 frrlem5.2 . . . . . . . . . 10 Se
23 sess2 4543 . . . . . . . . . 10 Se Se
2422, 23mpi 17 . . . . . . . . 9 Se
2521, 24jca 519 . . . . . . . 8 Se
2617, 18, 253syl 19 . . . . . . 7 Se
2726adantr 452 . . . . . 6 Se
2816frrlem4 25577 . . . . . 6
2916frrlem4 25577 . . . . . . . 8
3029ancoms 440 . . . . . . 7
31 incom 3525 . . . . . . . . . . 11
3231reseq2i 5135 . . . . . . . . . 10
3332fneq1i 5531 . . . . . . . . 9
3431fneq2i 5532 . . . . . . . . 9
3533, 34bitri 241 . . . . . . . 8
3632fveq1i 5721 . . . . . . . . . 10
37 predeq2 25434 . . . . . . . . . . . . 13
3831, 37ax-mp 8 . . . . . . . . . . . 12
3932, 38reseq12i 5136 . . . . . . . . . . 11
4039oveq2i 6084 . . . . . . . . . 10
4136, 40eqeq12i 2448 . . . . . . . . 9
4231, 41raleqbii 2727 . . . . . . . 8
4335, 42anbi12i 679 . . . . . . 7
4430, 43sylibr 204 . . . . . 6
45 frr3g 25573 . . . . . 6 Se
4627, 28, 44, 45syl3anc 1184 . . . . 5
4746breqd 4215 . . . 4
4847biimprd 215 . . 3
4916frrlem2 25575 . . . . 5
50 funres 5484 . . . . 5
51 dffun2 5456 . . . . . . 7
5251simprbi 451 . . . . . 6
53 sp 1763 . . . . . . . 8
5453sps 1770 . . . . . . 7
5554sps 1770 . . . . . 6
5652, 55syl 16 . . . . 5
5749, 50, 563syl 19 . . . 4