Step | Hyp | Ref
| Expression |
1 | | neiptop.o |
. . . . 5
β’ π½ = {π β π« π β£ βπ β π π β (πβπ)} |
2 | | neiptop.0 |
. . . . 5
β’ (π β π:πβΆπ« π« π) |
3 | | neiptop.1 |
. . . . 5
β’ ((((π β§ π β π) β§ π β π β§ π β π) β§ π β (πβπ)) β π β (πβπ)) |
4 | | neiptop.2 |
. . . . 5
β’ ((π β§ π β π) β (fiβ(πβπ)) β (πβπ)) |
5 | | neiptop.3 |
. . . . 5
β’ (((π β§ π β π) β§ π β (πβπ)) β π β π) |
6 | | neiptop.4 |
. . . . 5
β’ (((π β§ π β π) β§ π β (πβπ)) β βπ β (πβπ)βπ β π π β (πβπ)) |
7 | | neiptop.5 |
. . . . 5
β’ ((π β§ π β π) β π β (πβπ)) |
8 | 1, 2, 3, 4, 5, 6, 7 | neiptoptop 22855 |
. . . 4
β’ (π β π½ β Top) |
9 | | toptopon2 22640 |
. . . 4
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
10 | 8, 9 | sylib 217 |
. . 3
β’ (π β π½ β (TopOnββͺ π½)) |
11 | 1, 2, 3, 4, 5, 6, 7 | neiptopuni 22854 |
. . . 4
β’ (π β π = βͺ π½) |
12 | 11 | fveq2d 6894 |
. . 3
β’ (π β (TopOnβπ) = (TopOnββͺ π½)) |
13 | 10, 12 | eleqtrrd 2834 |
. 2
β’ (π β π½ β (TopOnβπ)) |
14 | 1, 2, 3, 4, 5, 6, 7 | neiptopnei 22856 |
. 2
β’ (π β π = (π β π β¦ ((neiβπ½)β{π}))) |
15 | | nfv 1915 |
. . . . . . . . . 10
β’
β²π(π β§ π β (TopOnβπ)) |
16 | | nfmpt1 5255 |
. . . . . . . . . . 11
β’
β²π(π β π β¦ ((neiβπ)β{π})) |
17 | 16 | nfeq2 2918 |
. . . . . . . . . 10
β’
β²π π = (π β π β¦ ((neiβπ)β{π})) |
18 | 15, 17 | nfan 1900 |
. . . . . . . . 9
β’
β²π((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) |
19 | | nfv 1915 |
. . . . . . . . 9
β’
β²π π β π |
20 | 18, 19 | nfan 1900 |
. . . . . . . 8
β’
β²π(((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) |
21 | | simpllr 772 |
. . . . . . . . . . 11
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β π = (π β π β¦ ((neiβπ)β{π}))) |
22 | | simpr 483 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β π β π) |
23 | 22 | sselda 3981 |
. . . . . . . . . . 11
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β π β π) |
24 | | id 22 |
. . . . . . . . . . . 12
β’ (π = (π β π β¦ ((neiβπ)β{π})) β π = (π β π β¦ ((neiβπ)β{π}))) |
25 | | fvexd 6905 |
. . . . . . . . . . . 12
β’ ((π = (π β π β¦ ((neiβπ)β{π})) β§ π β π) β ((neiβπ)β{π}) β V) |
26 | 24, 25 | fvmpt2d 7010 |
. . . . . . . . . . 11
β’ ((π = (π β π β¦ ((neiβπ)β{π})) β§ π β π) β (πβπ) = ((neiβπ)β{π})) |
27 | 21, 23, 26 | syl2anc 582 |
. . . . . . . . . 10
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β (πβπ) = ((neiβπ)β{π})) |
28 | 27 | eqcomd 2736 |
. . . . . . . . 9
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β ((neiβπ)β{π}) = (πβπ)) |
29 | 28 | eleq2d 2817 |
. . . . . . . 8
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β (π β ((neiβπ)β{π}) β π β (πβπ))) |
30 | 20, 29 | ralbida 3265 |
. . . . . . 7
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β (βπ β π π β ((neiβπ)β{π}) β βπ β π π β (πβπ))) |
31 | 30 | pm5.32da 577 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β ((π β π β§ βπ β π π β ((neiβπ)β{π})) β (π β π β§ βπ β π π β (πβπ)))) |
32 | | toponss 22649 |
. . . . . . . . 9
β’ ((π β (TopOnβπ) β§ π β π) β π β π) |
33 | 32 | ad4ant24 750 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β π β π) |
34 | | topontop 22635 |
. . . . . . . . . . 11
β’ (π β (TopOnβπ) β π β Top) |
35 | 34 | ad2antlr 723 |
. . . . . . . . . 10
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β π β Top) |
36 | | opnnei 22844 |
. . . . . . . . . 10
β’ (π β Top β (π β π β βπ β π π β ((neiβπ)β{π}))) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π β βπ β π π β ((neiβπ)β{π}))) |
38 | 37 | biimpa 475 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β βπ β π π β ((neiβπ)β{π})) |
39 | 33, 38 | jca 510 |
. . . . . . 7
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β (π β π β§ βπ β π π β ((neiβπ)β{π}))) |
40 | 37 | biimpar 476 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ βπ β π π β ((neiβπ)β{π})) β π β π) |
41 | 40 | adantrl 712 |
. . . . . . 7
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ (π β π β§ βπ β π π β ((neiβπ)β{π}))) β π β π) |
42 | 39, 41 | impbida 797 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π β (π β π β§ βπ β π π β ((neiβπ)β{π})))) |
43 | 1 | neipeltop 22853 |
. . . . . . 7
β’ (π β π½ β (π β π β§ βπ β π π β (πβπ))) |
44 | 43 | a1i 11 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π½ β (π β π β§ βπ β π π β (πβπ)))) |
45 | 31, 42, 44 | 3bitr4d 310 |
. . . . 5
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π β π β π½)) |
46 | 45 | eqrdv 2728 |
. . . 4
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β π = π½) |
47 | 46 | ex 411 |
. . 3
β’ ((π β§ π β (TopOnβπ)) β (π = (π β π β¦ ((neiβπ)β{π})) β π = π½)) |
48 | 47 | ralrimiva 3144 |
. 2
β’ (π β βπ β (TopOnβπ)(π = (π β π β¦ ((neiβπ)β{π})) β π = π½)) |
49 | | simpl 481 |
. . . . . . 7
β’ ((π = π½ β§ π β π) β π = π½) |
50 | 49 | fveq2d 6894 |
. . . . . 6
β’ ((π = π½ β§ π β π) β (neiβπ) = (neiβπ½)) |
51 | 50 | fveq1d 6892 |
. . . . 5
β’ ((π = π½ β§ π β π) β ((neiβπ)β{π}) = ((neiβπ½)β{π})) |
52 | 51 | mpteq2dva 5247 |
. . . 4
β’ (π = π½ β (π β π β¦ ((neiβπ)β{π})) = (π β π β¦ ((neiβπ½)β{π}))) |
53 | 52 | eqeq2d 2741 |
. . 3
β’ (π = π½ β (π = (π β π β¦ ((neiβπ)β{π})) β π = (π β π β¦ ((neiβπ½)β{π})))) |
54 | 53 | eqreu 3724 |
. 2
β’ ((π½ β (TopOnβπ) β§ π = (π β π β¦ ((neiβπ½)β{π})) β§ βπ β (TopOnβπ)(π = (π β π β¦ ((neiβπ)β{π})) β π = π½)) β β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π}))) |
55 | 13, 14, 48, 54 | syl3anc 1369 |
1
β’ (π β β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π}))) |