Step | Hyp | Ref
| Expression |
1 | | ptbas.1 |
. . . . . 6
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} |
2 | 1 | elpt 22939 |
. . . . 5
β’ (π β π΅ β βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))) |
3 | 1 | elpt 22939 |
. . . . 5
β’ (π β π΅ β βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))) |
4 | 2, 3 | anbi12i 628 |
. . . 4
β’ ((π β π΅ β§ π β π΅) β (βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)))) |
5 | | exdistrv 1960 |
. . . 4
β’
(βπβπ(((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))) β (βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)))) |
6 | 4, 5 | bitr4i 278 |
. . 3
β’ ((π β π΅ β§ π β π΅) β βπβπ(((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)))) |
7 | | an4 655 |
. . . . 5
β’ ((((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))) β (((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦))) β§ (π = Xπ¦ β π΄ (πβπ¦) β§ π = Xπ¦ β π΄ (πβπ¦)))) |
8 | | an6 1446 |
. . . . . . . . 9
β’ (((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦))) β ((π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦)) β§ (βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) |
9 | | df-3an 1090 |
. . . . . . . . 9
β’ (((π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦)) β§ (βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦))) β (((π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ (βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) |
10 | 8, 9 | bitri 275 |
. . . . . . . 8
β’ (((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦))) β (((π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ (βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) |
11 | | reeanv 3216 |
. . . . . . . . . . 11
β’
(βπ β Fin
βπ β Fin
(βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β (βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦))) |
12 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (πβπ¦) = (πβπ)) |
13 | | fveq2 6843 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (πβπ¦) = (πβπ)) |
14 | 12, 13 | ineq12d 4174 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((πβπ¦) β© (πβπ¦)) = ((πβπ) β© (πβπ))) |
15 | 14 | cbvixpv 8856 |
. . . . . . . . . . . . . 14
β’ Xπ¦ β
π΄ ((πβπ¦) β© (πβπ¦)) = Xπ β π΄ ((πβπ) β© (πβπ)) |
16 | | simpl1l 1225 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β π΄ β π) |
17 | | unfi 9119 |
. . . . . . . . . . . . . . . 16
β’ ((π β Fin β§ π β Fin) β (π βͺ π) β Fin) |
18 | 17 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β (π βͺ π) β Fin) |
19 | | simpl1r 1226 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β πΉ:π΄βΆTop) |
20 | 19 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β π΄) β (πΉβπ) β Top) |
21 | | simpl3l 1229 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β βπ¦ β π΄ (πβπ¦) β (πΉβπ¦)) |
22 | | fveq2 6843 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β (πΉβπ¦) = (πΉβπ)) |
23 | 12, 22 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β ((πβπ¦) β (πΉβπ¦) β (πβπ) β (πΉβπ))) |
24 | 23 | rspccva 3579 |
. . . . . . . . . . . . . . . . 17
β’
((βπ¦ β
π΄ (πβπ¦) β (πΉβπ¦) β§ π β π΄) β (πβπ) β (πΉβπ)) |
25 | 21, 24 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β π΄) β (πβπ) β (πΉβπ)) |
26 | | simpl3r 1230 |
. . . . . . . . . . . . . . . . 17
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β βπ¦ β π΄ (πβπ¦) β (πΉβπ¦)) |
27 | 13, 22 | eleq12d 2828 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ = π β ((πβπ¦) β (πΉβπ¦) β (πβπ) β (πΉβπ))) |
28 | 27 | rspccva 3579 |
. . . . . . . . . . . . . . . . 17
β’
((βπ¦ β
π΄ (πβπ¦) β (πΉβπ¦) β§ π β π΄) β (πβπ) β (πΉβπ)) |
29 | 26, 28 | sylan 581 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β π΄) β (πβπ) β (πΉβπ)) |
30 | | inopn 22264 |
. . . . . . . . . . . . . . . 16
β’ (((πΉβπ) β Top β§ (πβπ) β (πΉβπ) β§ (πβπ) β (πΉβπ)) β ((πβπ) β© (πβπ)) β (πΉβπ)) |
31 | 20, 25, 29, 30 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β π΄) β ((πβπ) β© (πβπ)) β (πΉβπ)) |
32 | | simprrl 780 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) |
33 | | ssun1 4133 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β (π βͺ π) |
34 | | sscon 4099 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π βͺ π) β (π΄ β (π βͺ π)) β (π΄ β π)) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β (π βͺ π)) β (π΄ β π) |
36 | 35 | sseli 3941 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ β (π βͺ π)) β π β (π΄ β π)) |
37 | 22 | unieqd 4880 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ = π β βͺ (πΉβπ¦) = βͺ (πΉβπ)) |
38 | 12, 37 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β ((πβπ¦) = βͺ (πΉβπ¦) β (πβπ) = βͺ (πΉβπ))) |
39 | 38 | rspccva 3579 |
. . . . . . . . . . . . . . . . . 18
β’
((βπ¦ β
(π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ π β (π΄ β π)) β (πβπ) = βͺ (πΉβπ)) |
40 | 32, 36, 39 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β (π΄ β (π βͺ π))) β (πβπ) = βͺ (πΉβπ)) |
41 | | simprrr 781 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) |
42 | | ssun2 4134 |
. . . . . . . . . . . . . . . . . . . 20
β’ π β (π βͺ π) |
43 | | sscon 4099 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π βͺ π) β (π΄ β (π βͺ π)) β (π΄ β π)) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β (π βͺ π)) β (π΄ β π) |
45 | 44 | sseli 3941 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄ β (π βͺ π)) β π β (π΄ β π)) |
46 | 13, 37 | eqeq12d 2749 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ = π β ((πβπ¦) = βͺ (πΉβπ¦) β (πβπ) = βͺ (πΉβπ))) |
47 | 46 | rspccva 3579 |
. . . . . . . . . . . . . . . . . 18
β’
((βπ¦ β
(π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ π β (π΄ β π)) β (πβπ) = βͺ (πΉβπ)) |
48 | 41, 45, 47 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β (π΄ β (π βͺ π))) β (πβπ) = βͺ (πΉβπ)) |
49 | 40, 48 | ineq12d 4174 |
. . . . . . . . . . . . . . . 16
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β (π΄ β (π βͺ π))) β ((πβπ) β© (πβπ)) = (βͺ (πΉβπ) β© βͺ (πΉβπ))) |
50 | | inidm 4179 |
. . . . . . . . . . . . . . . 16
β’ (βͺ (πΉβπ) β© βͺ (πΉβπ)) = βͺ (πΉβπ) |
51 | 49, 50 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β§ π β (π΄ β (π βͺ π))) β ((πβπ) β© (πβπ)) = βͺ (πΉβπ)) |
52 | 1, 16, 18, 31, 51 | elptr2 22941 |
. . . . . . . . . . . . . 14
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β Xπ β π΄ ((πβπ) β© (πβπ)) β π΅) |
53 | 15, 52 | eqeltrid 2838 |
. . . . . . . . . . . . 13
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ ((π β Fin β§ π β Fin) β§ (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅) |
54 | 53 | expr 458 |
. . . . . . . . . . . 12
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ (π β Fin β§ π β Fin)) β ((βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅)) |
55 | 54 | rexlimdvva 3202 |
. . . . . . . . . . 11
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β (βπ β Fin βπ β Fin (βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅)) |
56 | 11, 55 | biimtrrid 242 |
. . . . . . . . . 10
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β ((βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅)) |
57 | 56 | 3expb 1121 |
. . . . . . . . 9
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ ((π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦)))) β ((βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅)) |
58 | 57 | impr 456 |
. . . . . . . 8
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (((π Fn π΄ β§ π Fn π΄) β§ (βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦))) β§ (βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅) |
59 | 10, 58 | sylan2b 595 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅) |
60 | | ineq12 4168 |
. . . . . . . . 9
β’ ((π = Xπ¦ β π΄ (πβπ¦) β§ π = Xπ¦ β π΄ (πβπ¦)) β (π β© π) = (Xπ¦ β π΄ (πβπ¦) β© Xπ¦ β π΄ (πβπ¦))) |
61 | | ixpin 8864 |
. . . . . . . . 9
β’ Xπ¦ β
π΄ ((πβπ¦) β© (πβπ¦)) = (Xπ¦ β π΄ (πβπ¦) β© Xπ¦ β π΄ (πβπ¦)) |
62 | 60, 61 | eqtr4di 2791 |
. . . . . . . 8
β’ ((π = Xπ¦ β π΄ (πβπ¦) β§ π = Xπ¦ β π΄ (πβπ¦)) β (π β© π) = Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦))) |
63 | 62 | eleq1d 2819 |
. . . . . . 7
β’ ((π = Xπ¦ β π΄ (πβπ¦) β§ π = Xπ¦ β π΄ (πβπ¦)) β ((π β© π) β π΅ β Xπ¦ β π΄ ((πβπ¦) β© (πβπ¦)) β π΅)) |
64 | 59, 63 | syl5ibrcom 247 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)))) β ((π = Xπ¦ β π΄ (πβπ¦) β§ π = Xπ¦ β π΄ (πβπ¦)) β (π β© π) β π΅)) |
65 | 64 | expimpd 455 |
. . . . 5
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β ((((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ (π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦))) β§ (π = Xπ¦ β π΄ (πβπ¦) β§ π = Xπ¦ β π΄ (πβπ¦))) β (π β© π) β π΅)) |
66 | 7, 65 | biimtrid 241 |
. . . 4
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β ((((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))) β (π β© π) β π΅)) |
67 | 66 | exlimdvv 1938 |
. . 3
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β (βπβπ(((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦)) β§ ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ β Fin βπ¦ β (π΄ β π)(πβπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (πβπ¦))) β (π β© π) β π΅)) |
68 | 6, 67 | biimtrid 241 |
. 2
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β ((π β π΅ β§ π β π΅) β (π β© π) β π΅)) |
69 | 68 | imp 408 |
1
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (π β π΅ β§ π β π΅)) β (π β© π) β π΅) |