MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  precsexlem5 Structured version   Visualization version   GIF version

Theorem precsexlem5 28249
Description: Lemma for surreal reciprocals. Calculate the value of the recursive right function at a successor. (Contributed by Scott Fenton, 13-Mar-2025.)
Hypotheses
Ref Expression
precsexlem.1 ๐น = rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
precsexlem.2 ๐ฟ = (1st โˆ˜ ๐น)
precsexlem.3 ๐‘… = (2nd โˆ˜ ๐น)
Assertion
Ref Expression
precsexlem5 (๐ผ โˆˆ ฯ‰ โ†’ (๐‘…โ€˜suc ๐ผ) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})))
Distinct variable groups:   ๐ด,๐‘Ž,๐‘™,๐‘,๐‘Ÿ,๐‘ฅ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…   ๐น,๐‘™,๐‘   ๐ผ,๐‘Ž,๐‘™,๐‘,๐‘Ÿ,๐‘ฅ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…   ๐ฟ,๐‘Ž,๐‘™,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ   ๐‘…,๐‘Ž,๐‘™,๐‘Ÿ,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐‘…
Allowed substitution hints:   ๐ด(๐‘ฆ๐ฟ,๐‘ฆ๐‘…)   ๐‘…(๐‘ฅ,๐‘,๐‘ฆ๐ฟ)   ๐น(๐‘ฅ,๐‘Ÿ,๐‘Ž,๐‘ฅ๐ฟ,๐‘ฅ๐‘…,๐‘ฆ๐ฟ,๐‘ฆ๐‘…)   ๐ฟ(๐‘ฅ,๐‘Ÿ,๐‘,๐‘ฆ๐‘…)

Proof of Theorem precsexlem5
StepHypRef Expression
1 precsexlem.3 . . 3 ๐‘… = (2nd โˆ˜ ๐น)
21fveq1i 6907 . 2 (๐‘…โ€˜suc ๐ผ) = ((2nd โˆ˜ ๐น)โ€˜suc ๐ผ)
3 peano2 7912 . . . 4 (๐ผ โˆˆ ฯ‰ โ†’ suc ๐ผ โˆˆ ฯ‰)
4 nnon 7892 . . . 4 (suc ๐ผ โˆˆ ฯ‰ โ†’ suc ๐ผ โˆˆ On)
5 rdgfnon 8456 . . . . . 6 rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ) Fn On
6 precsexlem.1 . . . . . . 7 ๐น = rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ)
76fneq1i 6665 . . . . . 6 (๐น Fn On โ†” rec((๐‘ โˆˆ V โ†ฆ โฆ‹(1st โ€˜๐‘) / ๐‘™โฆŒโฆ‹(2nd โ€˜๐‘) / ๐‘ŸโฆŒโŸจ(๐‘™ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), (๐‘Ÿ โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ ๐‘™ ๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ ๐‘Ÿ ๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ), โŸจ{ 0s }, โˆ…โŸฉ) Fn On)
85, 7mpbir 231 . . . . 5 ๐น Fn On
9 fvco2 7005 . . . . 5 ((๐น Fn On โˆง suc ๐ผ โˆˆ On) โ†’ ((2nd โˆ˜ ๐น)โ€˜suc ๐ผ) = (2nd โ€˜(๐นโ€˜suc ๐ผ)))
108, 9mpan 690 . . . 4 (suc ๐ผ โˆˆ On โ†’ ((2nd โˆ˜ ๐น)โ€˜suc ๐ผ) = (2nd โ€˜(๐นโ€˜suc ๐ผ)))
113, 4, 103syl 18 . . 3 (๐ผ โˆˆ ฯ‰ โ†’ ((2nd โˆ˜ ๐น)โ€˜suc ๐ผ) = (2nd โ€˜(๐นโ€˜suc ๐ผ)))
12 precsexlem.2 . . . . . 6 ๐ฟ = (1st โˆ˜ ๐น)
136, 12, 1precsexlem3 28247 . . . . 5 (๐ผ โˆˆ ฯ‰ โ†’ (๐นโ€˜suc ๐ผ) = โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ)
1413fveq2d 6910 . . . 4 (๐ผ โˆˆ ฯ‰ โ†’ (2nd โ€˜(๐นโ€˜suc ๐ผ)) = (2nd โ€˜โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ))
15 fvex 6919 . . . . . 6 (๐ฟโ€˜๐ผ) โˆˆ V
16 fvex 6919 . . . . . . . 8 ( R โ€˜๐ด) โˆˆ V
1716, 15ab2rexex 8002 . . . . . . 7 {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆˆ V
18 fvex 6919 . . . . . . . . 9 ( L โ€˜๐ด) โˆˆ V
1918rabex 5344 . . . . . . . 8 {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ} โˆˆ V
20 fvex 6919 . . . . . . . 8 (๐‘…โ€˜๐ผ) โˆˆ V
2119, 20ab2rexex 8002 . . . . . . 7 {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)} โˆˆ V
2217, 21unex 7762 . . . . . 6 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)}) โˆˆ V
2315, 22unex 7762 . . . . 5 ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})) โˆˆ V
2419, 15ab2rexex 8002 . . . . . . 7 {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆˆ V
2516, 20ab2rexex 8002 . . . . . . 7 {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)} โˆˆ V
2624, 25unex 7762 . . . . . 6 ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}) โˆˆ V
2720, 26unex 7762 . . . . 5 ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})) โˆˆ V
2823, 27op2nd 8021 . . . 4 (2nd โ€˜โŸจ((๐ฟโ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐‘…)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐ฟ)})), ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))โŸฉ) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)}))
2914, 28eqtrdi 2790 . . 3 (๐ผ โˆˆ ฯ‰ โ†’ (2nd โ€˜(๐นโ€˜suc ๐ผ)) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})))
3011, 29eqtrd 2774 . 2 (๐ผ โˆˆ ฯ‰ โ†’ ((2nd โˆ˜ ๐น)โ€˜suc ๐ผ) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})))
312, 30eqtrid 2786 1 (๐ผ โˆˆ ฯ‰ โ†’ (๐‘…โ€˜suc ๐ผ) = ((๐‘…โ€˜๐ผ) โˆช ({๐‘Ž โˆฃ โˆƒ๐‘ฅ๐ฟ โˆˆ {๐‘ฅ โˆˆ ( L โ€˜๐ด) โˆฃ 0s <s ๐‘ฅ}โˆƒ๐‘ฆ๐ฟ โˆˆ (๐ฟโ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐ฟ -s ๐ด) ยทs ๐‘ฆ๐ฟ)) /su ๐‘ฅ๐ฟ)} โˆช {๐‘Ž โˆฃ โˆƒ๐‘ฅ๐‘… โˆˆ ( R โ€˜๐ด)โˆƒ๐‘ฆ๐‘… โˆˆ (๐‘…โ€˜๐ผ)๐‘Ž = (( 1s +s ((๐‘ฅ๐‘… -s ๐ด) ยทs ๐‘ฆ๐‘…)) /su ๐‘ฅ๐‘…)})))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   = wceq 1536   โˆˆ wcel 2105  {cab 2711  โˆƒwrex 3067  {crab 3432  Vcvv 3477  โฆ‹csb 3907   โˆช cun 3960  โˆ…c0 4338  {csn 4630  โŸจcop 4636   class class class wbr 5147   โ†ฆ cmpt 5230   โˆ˜ ccom 5692  Oncon0 6385  suc csuc 6387   Fn wfn 6557  โ€˜cfv 6562  (class class class)co 7430  ฯ‰com 7886  1st c1st 8010  2nd c2nd 8011  reccrdg 8447   <s cslt 27699   0s c0s 27881   1s c1s 27882   L cleft 27898   R cright 27899   +s cadds 28006   -s csubs 28066   ยทs cmuls 28146   /su cdivs 28227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448
This theorem is referenced by:  precsexlem7  28251  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255
  Copyright terms: Public domain W3C validator