Step | Hyp | Ref
| Expression |
1 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = 0 β ((β
Dπ πΉ)βπ₯) = ((β Dπ πΉ)β0)) |
2 | 1 | dmeqd 5906 |
. . . . . . . 8
β’ (π₯ = 0 β dom ((β
Dπ πΉ)βπ₯) = dom ((β Dπ πΉ)β0)) |
3 | 2 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = 0 β (dom ((β
Dπ πΉ)βπ₯) = dom πΉ β dom ((β Dπ
πΉ)β0) = dom πΉ)) |
4 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = 0 β ((π Dπ (πΉ βΎ π))βπ₯) = ((π Dπ (πΉ βΎ π))β0)) |
5 | 1 | reseq1d 5981 |
. . . . . . . 8
β’ (π₯ = 0 β (((β
Dπ πΉ)βπ₯) βΎ π) = (((β Dπ πΉ)β0) βΎ π)) |
6 | 4, 5 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = 0 β (((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π) β ((π Dπ (πΉ βΎ π))β0) = (((β
Dπ πΉ)β0) βΎ π))) |
7 | 3, 6 | imbi12d 345 |
. . . . . 6
β’ (π₯ = 0 β ((dom ((β
Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π)) β (dom ((β
Dπ πΉ)β0) = dom πΉ β ((π Dπ (πΉ βΎ π))β0) = (((β
Dπ πΉ)β0) βΎ π)))) |
8 | 7 | imbi2d 341 |
. . . . 5
β’ (π₯ = 0 β (((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π))) β ((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)β0) = dom πΉ β ((π Dπ (πΉ βΎ π))β0) = (((β
Dπ πΉ)β0) βΎ π))))) |
9 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = π β ((β Dπ πΉ)βπ₯) = ((β Dπ πΉ)βπ)) |
10 | 9 | dmeqd 5906 |
. . . . . . . 8
β’ (π₯ = π β dom ((β Dπ
πΉ)βπ₯) = dom ((β Dπ πΉ)βπ)) |
11 | 10 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = π β (dom ((β Dπ
πΉ)βπ₯) = dom πΉ β dom ((β Dπ
πΉ)βπ) = dom πΉ)) |
12 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = π β ((π Dπ (πΉ βΎ π))βπ₯) = ((π Dπ (πΉ βΎ π))βπ)) |
13 | 9 | reseq1d 5981 |
. . . . . . . 8
β’ (π₯ = π β (((β Dπ
πΉ)βπ₯) βΎ π) = (((β Dπ πΉ)βπ) βΎ π)) |
14 | 12, 13 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = π β (((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π) β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π))) |
15 | 11, 14 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π β ((dom ((β Dπ
πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π)) β (dom ((β
Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)))) |
16 | 15 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β (((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π))) β ((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π))))) |
17 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = (π + 1) β ((β Dπ
πΉ)βπ₯) = ((β Dπ πΉ)β(π + 1))) |
18 | 17 | dmeqd 5906 |
. . . . . . . 8
β’ (π₯ = (π + 1) β dom ((β
Dπ πΉ)βπ₯) = dom ((β Dπ πΉ)β(π + 1))) |
19 | 18 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = (π + 1) β (dom ((β
Dπ πΉ)βπ₯) = dom πΉ β dom ((β Dπ
πΉ)β(π + 1)) = dom πΉ)) |
20 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = (π + 1) β ((π Dπ (πΉ βΎ π))βπ₯) = ((π Dπ (πΉ βΎ π))β(π + 1))) |
21 | 17 | reseq1d 5981 |
. . . . . . . 8
β’ (π₯ = (π + 1) β (((β Dπ
πΉ)βπ₯) βΎ π) = (((β Dπ πΉ)β(π + 1)) βΎ π)) |
22 | 20, 21 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = (π + 1) β (((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π) β ((π Dπ (πΉ βΎ π))β(π + 1)) = (((β Dπ
πΉ)β(π + 1)) βΎ π))) |
23 | 19, 22 | imbi12d 345 |
. . . . . 6
β’ (π₯ = (π + 1) β ((dom ((β
Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π)) β (dom ((β
Dπ πΉ)β(π + 1)) = dom πΉ β ((π Dπ (πΉ βΎ π))β(π + 1)) = (((β Dπ
πΉ)β(π + 1)) βΎ π)))) |
24 | 23 | imbi2d 341 |
. . . . 5
β’ (π₯ = (π + 1) β (((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π))) β ((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)β(π + 1)) = dom πΉ β ((π Dπ (πΉ βΎ π))β(π + 1)) = (((β Dπ
πΉ)β(π + 1)) βΎ π))))) |
25 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = π β ((β Dπ
πΉ)βπ₯) = ((β Dπ πΉ)βπ)) |
26 | 25 | dmeqd 5906 |
. . . . . . . 8
β’ (π₯ = π β dom ((β Dπ
πΉ)βπ₯) = dom ((β Dπ πΉ)βπ)) |
27 | 26 | eqeq1d 2735 |
. . . . . . 7
β’ (π₯ = π β (dom ((β Dπ
πΉ)βπ₯) = dom πΉ β dom ((β Dπ
πΉ)βπ) = dom πΉ)) |
28 | | fveq2 6892 |
. . . . . . . 8
β’ (π₯ = π β ((π Dπ (πΉ βΎ π))βπ₯) = ((π Dπ (πΉ βΎ π))βπ)) |
29 | 25 | reseq1d 5981 |
. . . . . . . 8
β’ (π₯ = π β (((β Dπ
πΉ)βπ₯) βΎ π) = (((β Dπ πΉ)βπ) βΎ π)) |
30 | 28, 29 | eqeq12d 2749 |
. . . . . . 7
β’ (π₯ = π β (((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π) β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π))) |
31 | 27, 30 | imbi12d 345 |
. . . . . 6
β’ (π₯ = π β ((dom ((β
Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π)) β (dom ((β
Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)))) |
32 | 31 | imbi2d 341 |
. . . . 5
β’ (π₯ = π β (((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)βπ₯) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ₯) = (((β Dπ πΉ)βπ₯) βΎ π))) β ((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π))))) |
33 | | recnprss 25421 |
. . . . . . . . 9
β’ (π β {β, β}
β π β
β) |
34 | 33 | adantr 482 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β π β β) |
35 | | pmresg 8864 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β (πΉ βΎ π) β (β βpm π)) |
36 | | dvn0 25441 |
. . . . . . . 8
β’ ((π β β β§ (πΉ βΎ π) β (β βpm π)) β ((π Dπ (πΉ βΎ π))β0) = (πΉ βΎ π)) |
37 | 34, 35, 36 | syl2anc 585 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β ((π Dπ (πΉ βΎ π))β0) = (πΉ βΎ π)) |
38 | | ssidd 4006 |
. . . . . . . . 9
β’ (π β {β, β}
β β β β) |
39 | | dvn0 25441 |
. . . . . . . . 9
β’ ((β
β β β§ πΉ
β (β βpm β)) β ((β
Dπ πΉ)β0) = πΉ) |
40 | 38, 39 | sylan 581 |
. . . . . . . 8
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β ((β Dπ πΉ)β0) = πΉ) |
41 | 40 | reseq1d 5981 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β (((β Dπ πΉ)β0) βΎ π) = (πΉ βΎ π)) |
42 | 37, 41 | eqtr4d 2776 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β ((π Dπ (πΉ βΎ π))β0) = (((β
Dπ πΉ)β0) βΎ π)) |
43 | 42 | a1d 25 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)β0) = dom πΉ β ((π Dπ (πΉ βΎ π))β0) = (((β
Dπ πΉ)β0) βΎ π))) |
44 | | cnelprrecn 11203 |
. . . . . . . . . 10
β’ β
β {β, β} |
45 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β πΉ β (β βpm
β)) |
46 | | simprl 770 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β π β β0) |
47 | | dvnbss 25445 |
. . . . . . . . . 10
β’ ((β
β {β, β} β§ πΉ β (β βpm
β) β§ π β
β0) β dom ((β Dπ πΉ)βπ) β dom πΉ) |
48 | 44, 45, 46, 47 | mp3an2i 1467 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)βπ) β dom πΉ) |
49 | | simprr 772 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)β(π + 1)) = dom πΉ) |
50 | | ssidd 4006 |
. . . . . . . . . . . . 13
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β β β
β) |
51 | | dvnp1 25442 |
. . . . . . . . . . . . 13
β’ ((β
β β β§ πΉ
β (β βpm β) β§ π β β0) β ((β
Dπ πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
52 | 50, 45, 46, 51 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β ((β Dπ
πΉ)β(π + 1)) = (β D ((β
Dπ πΉ)βπ))) |
53 | 52 | dmeqd 5906 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)β(π + 1)) = dom (β D ((β
Dπ πΉ)βπ))) |
54 | 49, 53 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom πΉ = dom (β D ((β
Dπ πΉ)βπ))) |
55 | | dvnf 25444 |
. . . . . . . . . . . 12
β’ ((β
β {β, β} β§ πΉ β (β βpm
β) β§ π β
β0) β ((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) |
56 | 44, 45, 46, 55 | mp3an2i 1467 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β ((β Dπ
πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) |
57 | | cnex 11191 |
. . . . . . . . . . . . . . 15
β’ β
β V |
58 | 57, 57 | elpm2 8868 |
. . . . . . . . . . . . . 14
β’ (πΉ β (β
βpm β) β (πΉ:dom πΉβΆβ β§ dom πΉ β β)) |
59 | 58 | simprbi 498 |
. . . . . . . . . . . . 13
β’ (πΉ β (β
βpm β) β dom πΉ β β) |
60 | 45, 59 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom πΉ β β) |
61 | 48, 60 | sstrd 3993 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)βπ) β β) |
62 | 50, 56, 61 | dvbss 25418 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom (β D ((β
Dπ πΉ)βπ)) β dom ((β
Dπ πΉ)βπ)) |
63 | 54, 62 | eqsstrd 4021 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom πΉ β dom ((β Dπ
πΉ)βπ)) |
64 | 48, 63 | eqssd 4000 |
. . . . . . . 8
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)βπ) = dom πΉ) |
65 | 64 | expr 458 |
. . . . . . 7
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ π β β0) β (dom
((β Dπ πΉ)β(π + 1)) = dom πΉ β dom ((β Dπ
πΉ)βπ) = dom πΉ)) |
66 | 65 | imim1d 82 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ π β β0) β ((dom
((β Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)) β (dom ((β
Dπ πΉ)β(π + 1)) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)))) |
67 | | oveq2 7417 |
. . . . . . 7
β’ (((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π) β (π D ((π Dπ (πΉ βΎ π))βπ)) = (π D (((β Dπ πΉ)βπ) βΎ π))) |
68 | 34 | adantr 482 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β π β β) |
69 | 35 | adantr 482 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (πΉ βΎ π) β (β βpm π)) |
70 | | dvnp1 25442 |
. . . . . . . . 9
β’ ((π β β β§ (πΉ βΎ π) β (β βpm π) β§ π β β0) β ((π Dπ (πΉ βΎ π))β(π + 1)) = (π D ((π Dπ (πΉ βΎ π))βπ))) |
71 | 68, 69, 46, 70 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β ((π Dπ (πΉ βΎ π))β(π + 1)) = (π D ((π Dπ (πΉ βΎ π))βπ))) |
72 | 52 | reseq1d 5981 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (((β Dπ
πΉ)β(π + 1)) βΎ π) = ((β D ((β
Dπ πΉ)βπ)) βΎ π)) |
73 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β π β {β, β}) |
74 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(TopOpenββfld) =
(TopOpenββfld) |
75 | 74 | cnfldtop 24300 |
. . . . . . . . . . . . 13
β’
(TopOpenββfld) β Top |
76 | | unicntop 24302 |
. . . . . . . . . . . . . 14
β’ β =
βͺ
(TopOpenββfld) |
77 | 76 | ntrss2 22561 |
. . . . . . . . . . . . 13
β’
(((TopOpenββfld) β Top β§ dom ((β
Dπ πΉ)βπ) β β) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ)) β dom ((β
Dπ πΉ)βπ)) |
78 | 75, 61, 77 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ)) β dom ((β
Dπ πΉ)βπ)) |
79 | 74 | cnfldtopon 24299 |
. . . . . . . . . . . . . . . 16
β’
(TopOpenββfld) β
(TopOnββ) |
80 | 79 | toponrestid 22423 |
. . . . . . . . . . . . . . 15
β’
(TopOpenββfld) =
((TopOpenββfld) βΎt
β) |
81 | 50, 56, 61, 80, 74 | dvbssntr 25417 |
. . . . . . . . . . . . . 14
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom (β D ((β
Dπ πΉ)βπ)) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ))) |
82 | 54, 81 | eqsstrd 4021 |
. . . . . . . . . . . . 13
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom πΉ β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ))) |
83 | 48, 82 | sstrd 3993 |
. . . . . . . . . . . 12
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)βπ) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ))) |
84 | 78, 83 | eqssd 4000 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ)) = dom ((β Dπ
πΉ)βπ)) |
85 | 76 | isopn3 22570 |
. . . . . . . . . . . 12
β’
(((TopOpenββfld) β Top β§ dom ((β
Dπ πΉ)βπ) β β) β (dom ((β
Dπ πΉ)βπ) β
(TopOpenββfld) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ)) = dom ((β Dπ
πΉ)βπ))) |
86 | 75, 61, 85 | sylancr 588 |
. . . . . . . . . . 11
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (dom ((β
Dπ πΉ)βπ) β
(TopOpenββfld) β
((intβ(TopOpenββfld))βdom ((β
Dπ πΉ)βπ)) = dom ((β Dπ
πΉ)βπ))) |
87 | 84, 86 | mpbird 257 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom ((β
Dπ πΉ)βπ) β
(TopOpenββfld)) |
88 | 64, 54 | eqtr2d 2774 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β dom (β D ((β
Dπ πΉ)βπ)) = dom ((β Dπ
πΉ)βπ)) |
89 | 74 | dvres3a 25431 |
. . . . . . . . . 10
β’ (((π β {β, β} β§
((β Dπ πΉ)βπ):dom ((β Dπ πΉ)βπ)βΆβ) β§ (dom ((β
Dπ πΉ)βπ) β
(TopOpenββfld) β§ dom (β D ((β
Dπ πΉ)βπ)) = dom ((β Dπ
πΉ)βπ))) β (π D (((β Dπ πΉ)βπ) βΎ π)) = ((β D ((β
Dπ πΉ)βπ)) βΎ π)) |
90 | 73, 56, 87, 88, 89 | syl22anc 838 |
. . . . . . . . 9
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (π D (((β Dπ πΉ)βπ) βΎ π)) = ((β D ((β
Dπ πΉ)βπ)) βΎ π)) |
91 | 72, 90 | eqtr4d 2776 |
. . . . . . . 8
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (((β Dπ
πΉ)β(π + 1)) βΎ π) = (π D (((β Dπ πΉ)βπ) βΎ π))) |
92 | 71, 91 | eqeq12d 2749 |
. . . . . . 7
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (((π Dπ (πΉ βΎ π))β(π + 1)) = (((β Dπ
πΉ)β(π + 1)) βΎ π) β (π D ((π Dπ (πΉ βΎ π))βπ)) = (π D (((β Dπ πΉ)βπ) βΎ π)))) |
93 | 67, 92 | imbitrrid 245 |
. . . . . 6
β’ (((π β {β, β} β§
πΉ β (β
βpm β)) β§ (π β β0 β§ dom
((β Dπ πΉ)β(π + 1)) = dom πΉ)) β (((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π) β ((π Dπ (πΉ βΎ π))β(π + 1)) = (((β Dπ
πΉ)β(π + 1)) βΎ π))) |
94 | 66, 93 | animpimp2impd 845 |
. . . . 5
β’ (π β β0
β (((π β
{β, β} β§ πΉ
β (β βpm β)) β (dom ((β
Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π))) β ((π β {β, β} β§ πΉ β (β
βpm β)) β (dom ((β Dπ πΉ)β(π + 1)) = dom πΉ β ((π Dπ (πΉ βΎ π))β(π + 1)) = (((β Dπ
πΉ)β(π + 1)) βΎ π))))) |
95 | 8, 16, 24, 32, 43, 94 | nn0ind 12657 |
. . . 4
β’ (π β β0
β ((π β {β,
β} β§ πΉ β
(β βpm β)) β (dom ((β
Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)))) |
96 | 95 | com12 32 |
. . 3
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β (π β β0 β (dom
((β Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)))) |
97 | 96 | 3impia 1118 |
. 2
β’ ((π β {β, β} β§
πΉ β (β
βpm β) β§ π β β0) β (dom
((β Dπ πΉ)βπ) = dom πΉ β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π))) |
98 | 97 | imp 408 |
1
β’ (((π β {β, β} β§
πΉ β (β
βpm β) β§ π β β0) β§ dom
((β Dπ πΉ)βπ) = dom πΉ) β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)) |