Step | Hyp | Ref
| Expression |
1 | | cantnfval.h |
. . . 4
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
) |
2 | 1 | seqomsuc 8407 |
. . 3
โข (๐พ โ ฯ โ (๐ปโsuc ๐พ) = (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ))) |
3 | 2 | adantl 483 |
. 2
โข ((๐ โง ๐พ โ ฯ) โ (๐ปโsuc ๐พ) = (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ))) |
4 | | elex 3465 |
. . . 4
โข (๐พ โ ฯ โ ๐พ โ V) |
5 | 4 | adantl 483 |
. . 3
โข ((๐ โง ๐พ โ ฯ) โ ๐พ โ V) |
6 | | fvex 6859 |
. . 3
โข (๐ปโ๐พ) โ V |
7 | | simpl 484 |
. . . . . . . 8
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ ๐ข = ๐พ) |
8 | 7 | fveq2d 6850 |
. . . . . . 7
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (๐บโ๐ข) = (๐บโ๐พ)) |
9 | 8 | oveq2d 7377 |
. . . . . 6
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (๐ด โo (๐บโ๐ข)) = (๐ด โo (๐บโ๐พ))) |
10 | 8 | fveq2d 6850 |
. . . . . 6
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (๐นโ(๐บโ๐ข)) = (๐นโ(๐บโ๐พ))) |
11 | 9, 10 | oveq12d 7379 |
. . . . 5
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ ((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) = ((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ)))) |
12 | | simpr 486 |
. . . . 5
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ ๐ฃ = (๐ปโ๐พ)) |
13 | 11, 12 | oveq12d 7379 |
. . . 4
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ฃ) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |
14 | | fveq2 6846 |
. . . . . . . 8
โข (๐ = ๐ข โ (๐บโ๐) = (๐บโ๐ข)) |
15 | 14 | oveq2d 7377 |
. . . . . . 7
โข (๐ = ๐ข โ (๐ด โo (๐บโ๐)) = (๐ด โo (๐บโ๐ข))) |
16 | 14 | fveq2d 6850 |
. . . . . . 7
โข (๐ = ๐ข โ (๐นโ(๐บโ๐)) = (๐นโ(๐บโ๐ข))) |
17 | 15, 16 | oveq12d 7379 |
. . . . . 6
โข (๐ = ๐ข โ ((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) = ((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข)))) |
18 | 17 | oveq1d 7376 |
. . . . 5
โข (๐ = ๐ข โ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง) = (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ง)) |
19 | | oveq2 7369 |
. . . . 5
โข (๐ง = ๐ฃ โ (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ง) = (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ฃ)) |
20 | 18, 19 | cbvmpov 7456 |
. . . 4
โข (๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) = (๐ข โ V, ๐ฃ โ V โฆ (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ฃ)) |
21 | | ovex 7394 |
. . . 4
โข (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ)) โ V |
22 | 13, 20, 21 | ovmpoa 7514 |
. . 3
โข ((๐พ โ V โง (๐ปโ๐พ) โ V) โ (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ)) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |
23 | 5, 6, 22 | sylancl 587 |
. 2
โข ((๐ โง ๐พ โ ฯ) โ (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ)) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |
24 | 3, 23 | eqtrd 2773 |
1
โข ((๐ โง ๐พ โ ฯ) โ (๐ปโsuc ๐พ) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |