Step | Hyp | Ref
| Expression |
1 | | cantnfval.h |
. . . 4
โข ๐ป = seqฯ((๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)), โ
) |
2 | 1 | seqomsuc 8456 |
. . 3
โข (๐พ โ ฯ โ (๐ปโsuc ๐พ) = (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ))) |
3 | 2 | adantl 482 |
. 2
โข ((๐ โง ๐พ โ ฯ) โ (๐ปโsuc ๐พ) = (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ))) |
4 | | elex 3492 |
. . . 4
โข (๐พ โ ฯ โ ๐พ โ V) |
5 | 4 | adantl 482 |
. . 3
โข ((๐ โง ๐พ โ ฯ) โ ๐พ โ V) |
6 | | fvex 6904 |
. . 3
โข (๐ปโ๐พ) โ V |
7 | | simpl 483 |
. . . . . . . 8
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ ๐ข = ๐พ) |
8 | 7 | fveq2d 6895 |
. . . . . . 7
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (๐บโ๐ข) = (๐บโ๐พ)) |
9 | 8 | oveq2d 7424 |
. . . . . 6
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (๐ด โo (๐บโ๐ข)) = (๐ด โo (๐บโ๐พ))) |
10 | 8 | fveq2d 6895 |
. . . . . 6
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (๐นโ(๐บโ๐ข)) = (๐นโ(๐บโ๐พ))) |
11 | 9, 10 | oveq12d 7426 |
. . . . 5
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ ((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) = ((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ)))) |
12 | | simpr 485 |
. . . . 5
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ ๐ฃ = (๐ปโ๐พ)) |
13 | 11, 12 | oveq12d 7426 |
. . . 4
โข ((๐ข = ๐พ โง ๐ฃ = (๐ปโ๐พ)) โ (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ฃ) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |
14 | | fveq2 6891 |
. . . . . . . 8
โข (๐ = ๐ข โ (๐บโ๐) = (๐บโ๐ข)) |
15 | 14 | oveq2d 7424 |
. . . . . . 7
โข (๐ = ๐ข โ (๐ด โo (๐บโ๐)) = (๐ด โo (๐บโ๐ข))) |
16 | 14 | fveq2d 6895 |
. . . . . . 7
โข (๐ = ๐ข โ (๐นโ(๐บโ๐)) = (๐นโ(๐บโ๐ข))) |
17 | 15, 16 | oveq12d 7426 |
. . . . . 6
โข (๐ = ๐ข โ ((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) = ((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข)))) |
18 | 17 | oveq1d 7423 |
. . . . 5
โข (๐ = ๐ข โ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง) = (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ง)) |
19 | | oveq2 7416 |
. . . . 5
โข (๐ง = ๐ฃ โ (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ง) = (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ฃ)) |
20 | 18, 19 | cbvmpov 7503 |
. . . 4
โข (๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง)) = (๐ข โ V, ๐ฃ โ V โฆ (((๐ด โo (๐บโ๐ข)) ยทo (๐นโ(๐บโ๐ข))) +o ๐ฃ)) |
21 | | ovex 7441 |
. . . 4
โข (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ)) โ V |
22 | 13, 20, 21 | ovmpoa 7562 |
. . 3
โข ((๐พ โ V โง (๐ปโ๐พ) โ V) โ (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ)) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |
23 | 5, 6, 22 | sylancl 586 |
. 2
โข ((๐ โง ๐พ โ ฯ) โ (๐พ(๐ โ V, ๐ง โ V โฆ (((๐ด โo (๐บโ๐)) ยทo (๐นโ(๐บโ๐))) +o ๐ง))(๐ปโ๐พ)) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |
24 | 3, 23 | eqtrd 2772 |
1
โข ((๐ โง ๐พ โ ฯ) โ (๐ปโsuc ๐พ) = (((๐ด โo (๐บโ๐พ)) ยทo (๐นโ(๐บโ๐พ))) +o (๐ปโ๐พ))) |