Step | Hyp | Ref
| Expression |
1 | | ptbasfi.2 |
. . 3
β’ π = Xπ β π΄ βͺ (πΉβπ) |
2 | 1 | ptpjpre1 23430 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (β‘(π€ β π β¦ (π€βπΌ)) β π) = Xπ β π΄ if(π = πΌ, π, βͺ (πΉβπ))) |
3 | | ptbas.1 |
. . 3
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} |
4 | | simpll 764 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β π΄ β π) |
5 | | snfi 9046 |
. . . 4
β’ {πΌ} β Fin |
6 | 5 | a1i 11 |
. . 3
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β {πΌ} β Fin) |
7 | | simprr 770 |
. . . . . 6
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β π β (πΉβπΌ)) |
8 | 7 | ad2antrr 723 |
. . . . 5
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β§ π = πΌ) β π β (πΉβπΌ)) |
9 | | simpr 484 |
. . . . . 6
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β§ π = πΌ) β π = πΌ) |
10 | 9 | fveq2d 6889 |
. . . . 5
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β§ π = πΌ) β (πΉβπ) = (πΉβπΌ)) |
11 | 8, 10 | eleqtrrd 2830 |
. . . 4
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β§ π = πΌ) β π β (πΉβπ)) |
12 | | simplr 766 |
. . . . . . 7
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β πΉ:π΄βΆTop) |
13 | 12 | ffvelcdmda 7080 |
. . . . . 6
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β (πΉβπ) β Top) |
14 | | eqid 2726 |
. . . . . . 7
β’ βͺ (πΉβπ) = βͺ (πΉβπ) |
15 | 14 | topopn 22763 |
. . . . . 6
β’ ((πΉβπ) β Top β βͺ (πΉβπ) β (πΉβπ)) |
16 | 13, 15 | syl 17 |
. . . . 5
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β βͺ (πΉβπ) β (πΉβπ)) |
17 | 16 | adantr 480 |
. . . 4
β’
(((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β§ Β¬ π = πΌ) β βͺ (πΉβπ) β (πΉβπ)) |
18 | 11, 17 | ifclda 4558 |
. . 3
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β π΄) β if(π = πΌ, π, βͺ (πΉβπ)) β (πΉβπ)) |
19 | | eldifsni 4788 |
. . . . . 6
β’ (π β (π΄ β {πΌ}) β π β πΌ) |
20 | 19 | neneqd 2939 |
. . . . 5
β’ (π β (π΄ β {πΌ}) β Β¬ π = πΌ) |
21 | 20 | adantl 481 |
. . . 4
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β (π΄ β {πΌ})) β Β¬ π = πΌ) |
22 | 21 | iffalsed 4534 |
. . 3
β’ ((((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β§ π β (π΄ β {πΌ})) β if(π = πΌ, π, βͺ (πΉβπ)) = βͺ (πΉβπ)) |
23 | 3, 4, 6, 18, 22 | elptr2 23433 |
. 2
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β Xπ β π΄ if(π = πΌ, π, βͺ (πΉβπ)) β π΅) |
24 | 2, 23 | eqeltrd 2827 |
1
β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (β‘(π€ β π β¦ (π€βπΌ)) β π) β π΅) |