Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = 0 β ((β
Dπ πΉ)βπ₯) = ((β Dπ πΉ)β0)) |
2 | 1 | dmeqd 5906 |
. . . . . 6
β’ (π₯ = 0 β dom ((β
Dπ πΉ)βπ₯) = dom ((β Dπ πΉ)β0)) |
3 | 1, 2 | feq12d 6706 |
. . . . 5
β’ (π₯ = 0 β (((β
Dπ πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ β ((β
Dπ πΉ)β0):dom ((β
Dπ πΉ)β0)βΆβ)) |
4 | 3 | imbi2d 341 |
. . . 4
β’ (π₯ = 0 β (((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ) β ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)β0):dom ((β
Dπ πΉ)β0)βΆβ))) |
5 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = π β ((β Dπ πΉ)βπ₯) = ((β Dπ πΉ)βπ)) |
6 | 5 | dmeqd 5906 |
. . . . . 6
β’ (π₯ = π β dom ((β Dπ
πΉ)βπ₯) = dom ((β Dπ πΉ)βπ)) |
7 | 5, 6 | feq12d 6706 |
. . . . 5
β’ (π₯ = π β (((β Dπ
πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ β ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) |
8 | 7 | imbi2d 341 |
. . . 4
β’ (π₯ = π β (((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ) β ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ))) |
9 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = (π + 1) β ((β Dπ
πΉ)βπ₯) = ((β Dπ πΉ)β(π + 1))) |
10 | 9 | dmeqd 5906 |
. . . . . 6
β’ (π₯ = (π + 1) β dom ((β
Dπ πΉ)βπ₯) = dom ((β Dπ πΉ)β(π + 1))) |
11 | 9, 10 | feq12d 6706 |
. . . . 5
β’ (π₯ = (π + 1) β (((β Dπ
πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ β ((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π +
1))βΆβ)) |
12 | 11 | imbi2d 341 |
. . . 4
β’ (π₯ = (π + 1) β (((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ) β ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π +
1))βΆβ))) |
13 | | fveq2 6892 |
. . . . . 6
β’ (π₯ = π β ((β Dπ
πΉ)βπ₯) = ((β Dπ πΉ)βπ)) |
14 | 13 | dmeqd 5906 |
. . . . . 6
β’ (π₯ = π β dom ((β Dπ
πΉ)βπ₯) = dom ((β Dπ πΉ)βπ)) |
15 | 13, 14 | feq12d 6706 |
. . . . 5
β’ (π₯ = π β (((β Dπ
πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ β ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) |
16 | 15 | imbi2d 341 |
. . . 4
β’ (π₯ = π β (((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)βπ₯):dom ((β Dπ πΉ)βπ₯)βΆβ) β ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ))) |
17 | | simpl 484 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ:π΄βΆβ) |
18 | | ax-resscn 11167 |
. . . . . . 7
β’ β
β β |
19 | | fss 6735 |
. . . . . . . . 9
β’ ((πΉ:π΄βΆβ β§ β β
β) β πΉ:π΄βΆβ) |
20 | 18, 19 | mpan2 690 |
. . . . . . . 8
β’ (πΉ:π΄βΆβ β πΉ:π΄βΆβ) |
21 | | cnex 11191 |
. . . . . . . . 9
β’ β
β V |
22 | | reex 11201 |
. . . . . . . . 9
β’ β
β V |
23 | | elpm2r 8839 |
. . . . . . . . 9
β’
(((β β V β§ β β V) β§ (πΉ:π΄βΆβ β§ π΄ β β)) β πΉ β (β βpm
β)) |
24 | 21, 22, 23 | mpanl12 701 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
25 | 20, 24 | sylan 581 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β πΉ β (β βpm
β)) |
26 | | dvn0 25441 |
. . . . . . 7
β’ ((β
β β β§ πΉ
β (β βpm β)) β ((β
Dπ πΉ)β0) = πΉ) |
27 | 18, 25, 26 | sylancr 588 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)β0) = πΉ) |
28 | 27 | dmeqd 5906 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β dom ((β
Dπ πΉ)β0) = dom πΉ) |
29 | | fdm 6727 |
. . . . . . . 8
β’ (πΉ:π΄βΆβ β dom πΉ = π΄) |
30 | 29 | adantr 482 |
. . . . . . 7
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β dom πΉ = π΄) |
31 | 28, 30 | eqtrd 2773 |
. . . . . 6
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β dom ((β
Dπ πΉ)β0) = π΄) |
32 | 27, 31 | feq12d 6706 |
. . . . 5
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (((β
Dπ πΉ)β0):dom ((β
Dπ πΉ)β0)βΆβ β πΉ:π΄βΆβ)) |
33 | 17, 32 | mpbird 257 |
. . . 4
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)β0):dom ((β
Dπ πΉ)β0)βΆβ) |
34 | | simprr 772 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) |
35 | 22 | prid1 4767 |
. . . . . . . . . . . 12
β’ β
β {β, β} |
36 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β π β β0) |
37 | | dvnbss 25445 |
. . . . . . . . . . . 12
β’ ((β
β {β, β} β§ πΉ β (β βpm
β) β§ π β
β0) β dom ((β Dπ πΉ)βπ) β dom πΉ) |
38 | 35, 25, 36, 37 | mp3an2ani 1469 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β dom ((β
Dπ πΉ)βπ) β dom πΉ) |
39 | 30 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β dom πΉ = π΄) |
40 | 38, 39 | sseqtrd 4023 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β dom ((β
Dπ πΉ)βπ) β π΄) |
41 | | simplr 768 |
. . . . . . . . . 10
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β π΄ β β) |
42 | 40, 41 | sstrd 3993 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β dom ((β
Dπ πΉ)βπ) β β) |
43 | | dvfre 25468 |
. . . . . . . . 9
β’
((((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ β§ dom ((β
Dπ πΉ)βπ) β β) β (β D
((β Dπ πΉ)βπ)):dom (β D ((β
Dπ πΉ)βπ))βΆβ) |
44 | 34, 42, 43 | syl2anc 585 |
. . . . . . . 8
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β (β D
((β Dπ πΉ)βπ)):dom (β D ((β
Dπ πΉ)βπ))βΆβ) |
45 | | dvnp1 25442 |
. . . . . . . . . 10
β’ ((β
β β β§ πΉ
β (β βpm β) β§ π β β0) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
46 | 18, 25, 36, 45 | mp3an2ani 1469 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
47 | 46 | dmeqd 5906 |
. . . . . . . . 9
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β dom ((β
Dπ πΉ)β(π + 1)) = dom (β D ((β
Dπ πΉ)βπ))) |
48 | 46, 47 | feq12d 6706 |
. . . . . . . 8
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β (((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π + 1))βΆβ β
(β D ((β Dπ πΉ)βπ)):dom (β D ((β
Dπ πΉ)βπ))βΆβ)) |
49 | 44, 48 | mpbird 257 |
. . . . . . 7
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ (π β β0 β§ ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) β ((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π +
1))βΆβ) |
50 | 49 | expr 458 |
. . . . . 6
β’ (((πΉ:π΄βΆβ β§ π΄ β β) β§ π β β0) β
(((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ β ((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π +
1))βΆβ)) |
51 | 50 | expcom 415 |
. . . . 5
β’ (π β β0
β ((πΉ:π΄βΆβ β§ π΄ β β) β
(((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ β ((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π +
1))βΆβ))) |
52 | 51 | a2d 29 |
. . . 4
β’ (π β β0
β (((πΉ:π΄βΆβ β§ π΄ β β) β
((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) β ((πΉ:π΄βΆβ β§ π΄ β β) β ((β
Dπ πΉ)β(π + 1)):dom ((β Dπ
πΉ)β(π +
1))βΆβ))) |
53 | 4, 8, 12, 16, 33, 52 | nn0ind 12657 |
. . 3
β’ (π β β0
β ((πΉ:π΄βΆβ β§ π΄ β β) β
((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) |
54 | 53 | com12 32 |
. 2
β’ ((πΉ:π΄βΆβ β§ π΄ β β) β (π β β0 β ((β
Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ)) |
55 | 54 | 3impia 1118 |
1
β’ ((πΉ:π΄βΆβ β§ π΄ β β β§ π β β0) β
((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) |