Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β πΉ β
((πCπββ)βπ)) |
2 | | ssid 3970 |
. . . . . 6
β’ β
β β |
3 | | elfvdm 6883 |
. . . . . . . 8
β’ (πΉ β
((πCπββ)βπ) β π β dom
(πCπββ)) |
4 | 3 | adantl 483 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β π β dom
(πCπββ)) |
5 | | fncpn 25320 |
. . . . . . . . 9
β’ (β
β β β (πCπββ) Fn
β0) |
6 | 2, 5 | ax-mp 5 |
. . . . . . . 8
β’
(πCπββ) Fn
β0 |
7 | | fndm 6609 |
. . . . . . . 8
β’
((πCπββ) Fn β0
β dom (πCπββ) =
β0) |
8 | 6, 7 | mp1i 13 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β dom
(πCπββ) =
β0) |
9 | 4, 8 | eleqtrd 2836 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β π β
β0) |
10 | | elcpn 25321 |
. . . . . 6
β’ ((β
β β β§ π
β β0) β (πΉ β
((πCπββ)βπ) β (πΉ β (β βpm
β) β§ ((β Dπ πΉ)βπ) β (dom πΉβcnββ)))) |
11 | 2, 9, 10 | sylancr 588 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (πΉ β
((πCπββ)βπ) β (πΉ β (β βpm
β) β§ ((β Dπ πΉ)βπ) β (dom πΉβcnββ)))) |
12 | 1, 11 | mpbid 231 |
. . . 4
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (πΉ β (β βpm
β) β§ ((β Dπ πΉ)βπ) β (dom πΉβcnββ))) |
13 | 12 | simpld 496 |
. . 3
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β πΉ β (β βpm
β)) |
14 | | pmresg 8814 |
. . 3
β’ ((π β {β, β} β§
πΉ β (β
βpm β)) β (πΉ βΎ π) β (β βpm π)) |
15 | 13, 14 | syldan 592 |
. 2
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (πΉ βΎ π) β (β βpm π)) |
16 | | simpl 484 |
. . . 4
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β π β {β, β}) |
17 | 12 | simprd 497 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β ((β Dπ
πΉ)βπ) β (dom πΉβcnββ)) |
18 | | cncff 24279 |
. . . . . 6
β’
(((β Dπ πΉ)βπ) β (dom πΉβcnββ) β ((β Dπ
πΉ)βπ):dom πΉβΆβ) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β ((β Dπ
πΉ)βπ):dom πΉβΆβ) |
20 | 19 | fdmd 6683 |
. . . 4
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β dom ((β
Dπ πΉ)βπ) = dom πΉ) |
21 | | dvnres 25318 |
. . . 4
β’ (((π β {β, β} β§
πΉ β (β
βpm β) β§ π β β0) β§ dom
((β Dπ πΉ)βπ) = dom πΉ) β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)) |
22 | 16, 13, 9, 20, 21 | syl31anc 1374 |
. . 3
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β ((π Dπ (πΉ βΎ π))βπ) = (((β Dπ πΉ)βπ) βΎ π)) |
23 | | resres 5954 |
. . . . . . 7
β’
((((β Dπ πΉ)βπ) βΎ π) βΎ dom πΉ) = (((β Dπ πΉ)βπ) βΎ (π β© dom πΉ)) |
24 | | rescom 5967 |
. . . . . . 7
β’
((((β Dπ πΉ)βπ) βΎ π) βΎ dom πΉ) = ((((β Dπ πΉ)βπ) βΎ dom πΉ) βΎ π) |
25 | 23, 24 | eqtr3i 2763 |
. . . . . 6
β’
(((β Dπ πΉ)βπ) βΎ (π β© dom πΉ)) = ((((β Dπ πΉ)βπ) βΎ dom πΉ) βΎ π) |
26 | | ffn 6672 |
. . . . . . . 8
β’
(((β Dπ πΉ)βπ):dom πΉβΆβ β ((β
Dπ πΉ)βπ) Fn dom πΉ) |
27 | | fnresdm 6624 |
. . . . . . . 8
β’
(((β Dπ πΉ)βπ) Fn dom πΉ β (((β Dπ
πΉ)βπ) βΎ dom πΉ) = ((β Dπ πΉ)βπ)) |
28 | 19, 26, 27 | 3syl 18 |
. . . . . . 7
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (((β Dπ
πΉ)βπ) βΎ dom πΉ) = ((β Dπ πΉ)βπ)) |
29 | 28 | reseq1d 5940 |
. . . . . 6
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β ((((β Dπ
πΉ)βπ) βΎ dom πΉ) βΎ π) = (((β Dπ πΉ)βπ) βΎ π)) |
30 | 25, 29 | eqtrid 2785 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (((β Dπ
πΉ)βπ) βΎ (π β© dom πΉ)) = (((β Dπ πΉ)βπ) βΎ π)) |
31 | | inss2 4193 |
. . . . . 6
β’ (π β© dom πΉ) β dom πΉ |
32 | | rescncf 24283 |
. . . . . 6
β’ ((π β© dom πΉ) β dom πΉ β (((β Dπ
πΉ)βπ) β (dom πΉβcnββ) β (((β Dπ
πΉ)βπ) βΎ (π β© dom πΉ)) β ((π β© dom πΉ)βcnββ))) |
33 | 31, 17, 32 | mpsyl 68 |
. . . . 5
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (((β Dπ
πΉ)βπ) βΎ (π β© dom πΉ)) β ((π β© dom πΉ)βcnββ)) |
34 | 30, 33 | eqeltrrd 2835 |
. . . 4
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (((β Dπ
πΉ)βπ) βΎ π) β ((π β© dom πΉ)βcnββ)) |
35 | | dmres 5963 |
. . . . 5
β’ dom
(πΉ βΎ π) = (π β© dom πΉ) |
36 | 35 | oveq1i 7371 |
. . . 4
β’ (dom
(πΉ βΎ π)βcnββ) = ((π β© dom πΉ)βcnββ) |
37 | 34, 36 | eleqtrrdi 2845 |
. . 3
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (((β Dπ
πΉ)βπ) βΎ π) β (dom (πΉ βΎ π)βcnββ)) |
38 | 22, 37 | eqeltrd 2834 |
. 2
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β ((π Dπ (πΉ βΎ π))βπ) β (dom (πΉ βΎ π)βcnββ)) |
39 | | recnprss 25291 |
. . 3
β’ (π β {β, β}
β π β
β) |
40 | | elcpn 25321 |
. . 3
β’ ((π β β β§ π β β0)
β ((πΉ βΎ π) β
((πCπβπ)βπ) β ((πΉ βΎ π) β (β βpm π) β§ ((π Dπ (πΉ βΎ π))βπ) β (dom (πΉ βΎ π)βcnββ)))) |
41 | 39, 9, 40 | syl2an2r 684 |
. 2
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β ((πΉ βΎ π) β
((πCπβπ)βπ) β ((πΉ βΎ π) β (β βpm π) β§ ((π Dπ (πΉ βΎ π))βπ) β (dom (πΉ βΎ π)βcnββ)))) |
42 | 15, 38, 41 | mpbir2and 712 |
1
β’ ((π β {β, β} β§
πΉ β
((πCπββ)βπ)) β (πΉ βΎ π) β
((πCπβπ)βπ)) |