Step | Hyp | Ref
| Expression |
1 | | reldv 25257 |
. 2
β’ Rel
(π D (πΉ βΎ π΅)) |
2 | | relres 5970 |
. 2
β’ Rel
((π D πΉ) βΎ ((intβπ)βπ΅)) |
3 | | simpll 766 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β π β β) |
4 | | simplr 768 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β πΉ:π΄βΆβ) |
5 | | inss1 4192 |
. . . . . . . 8
β’ (π΄ β© π΅) β π΄ |
6 | | fssres 6712 |
. . . . . . . 8
β’ ((πΉ:π΄βΆβ β§ (π΄ β© π΅) β π΄) β (πΉ βΎ (π΄ β© π΅)):(π΄ β© π΅)βΆβ) |
7 | 4, 5, 6 | sylancl 587 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (πΉ βΎ (π΄ β© π΅)):(π΄ β© π΅)βΆβ) |
8 | | resres 5954 |
. . . . . . . . 9
β’ ((πΉ βΎ π΄) βΎ π΅) = (πΉ βΎ (π΄ β© π΅)) |
9 | | ffn 6672 |
. . . . . . . . . . 11
β’ (πΉ:π΄βΆβ β πΉ Fn π΄) |
10 | | fnresdm 6624 |
. . . . . . . . . . 11
β’ (πΉ Fn π΄ β (πΉ βΎ π΄) = πΉ) |
11 | 4, 9, 10 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (πΉ βΎ π΄) = πΉ) |
12 | 11 | reseq1d 5940 |
. . . . . . . . 9
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β ((πΉ βΎ π΄) βΎ π΅) = (πΉ βΎ π΅)) |
13 | 8, 12 | eqtr3id 2787 |
. . . . . . . 8
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (πΉ βΎ (π΄ β© π΅)) = (πΉ βΎ π΅)) |
14 | 13 | feq1d 6657 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β ((πΉ βΎ (π΄ β© π΅)):(π΄ β© π΅)βΆβ β (πΉ βΎ π΅):(π΄ β© π΅)βΆβ)) |
15 | 7, 14 | mpbid 231 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (πΉ βΎ π΅):(π΄ β© π΅)βΆβ) |
16 | | simprl 770 |
. . . . . . 7
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β π΄ β π) |
17 | 5, 16 | sstrid 3959 |
. . . . . 6
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π΄ β© π΅) β π) |
18 | 3, 15, 17 | dvcl 25286 |
. . . . 5
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π₯(π D (πΉ βΎ π΅))π¦) β π¦ β β) |
19 | 18 | ex 414 |
. . . 4
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π₯(π D (πΉ βΎ π΅))π¦ β π¦ β β)) |
20 | 3, 4, 16 | dvcl 25286 |
. . . . . 6
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π₯(π D πΉ)π¦) β π¦ β β) |
21 | 20 | ex 414 |
. . . . 5
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π₯(π D πΉ)π¦ β π¦ β β)) |
22 | 21 | adantld 492 |
. . . 4
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β ((π₯ β ((intβπ)βπ΅) β§ π₯(π D πΉ)π¦) β π¦ β β)) |
23 | | dvres.k |
. . . . . 6
β’ πΎ =
(TopOpenββfld) |
24 | | dvres.t |
. . . . . 6
β’ π = (πΎ βΎt π) |
25 | | eqid 2733 |
. . . . . 6
β’ (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) = (π§ β (π΄ β {π₯}) β¦ (((πΉβπ§) β (πΉβπ₯)) / (π§ β π₯))) |
26 | 3 | adantr 482 |
. . . . . 6
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π¦ β β) β π β β) |
27 | 4 | adantr 482 |
. . . . . 6
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π¦ β β) β πΉ:π΄βΆβ) |
28 | 16 | adantr 482 |
. . . . . 6
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π¦ β β) β π΄ β π) |
29 | | simplrr 777 |
. . . . . 6
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π¦ β β) β π΅ β π) |
30 | | simpr 486 |
. . . . . 6
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π¦ β β) β π¦ β β) |
31 | 23, 24, 25, 26, 27, 28, 29, 30 | dvreslem 25296 |
. . . . 5
β’ ((((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β§ π¦ β β) β (π₯(π D (πΉ βΎ π΅))π¦ β (π₯ β ((intβπ)βπ΅) β§ π₯(π D πΉ)π¦))) |
32 | 31 | ex 414 |
. . . 4
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π¦ β β β (π₯(π D (πΉ βΎ π΅))π¦ β (π₯ β ((intβπ)βπ΅) β§ π₯(π D πΉ)π¦)))) |
33 | 19, 22, 32 | pm5.21ndd 381 |
. . 3
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π₯(π D (πΉ βΎ π΅))π¦ β (π₯ β ((intβπ)βπ΅) β§ π₯(π D πΉ)π¦))) |
34 | | vex 3451 |
. . . 4
β’ π¦ β V |
35 | 34 | brresi 5950 |
. . 3
β’ (π₯((π D πΉ) βΎ ((intβπ)βπ΅))π¦ β (π₯ β ((intβπ)βπ΅) β§ π₯(π D πΉ)π¦)) |
36 | 33, 35 | bitr4di 289 |
. 2
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π₯(π D (πΉ βΎ π΅))π¦ β π₯((π D πΉ) βΎ ((intβπ)βπ΅))π¦)) |
37 | 1, 2, 36 | eqbrrdiv 5754 |
1
β’ (((π β β β§ πΉ:π΄βΆβ) β§ (π΄ β π β§ π΅ β π)) β (π D (πΉ βΎ π΅)) = ((π D πΉ) βΎ ((intβπ)βπ΅))) |