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 22635 |
. . . 4
β’ (π β π½ β Top) |
9 | | toptopon2 22420 |
. . . 4
β’ (π½ β Top β π½ β (TopOnββͺ π½)) |
10 | 8, 9 | sylib 217 |
. . 3
β’ (π β π½ β (TopOnββͺ π½)) |
11 | 1, 2, 3, 4, 5, 6, 7 | neiptopuni 22634 |
. . . 4
β’ (π β π = βͺ π½) |
12 | 11 | fveq2d 6896 |
. . 3
β’ (π β (TopOnβπ) = (TopOnββͺ π½)) |
13 | 10, 12 | eleqtrrd 2837 |
. 2
β’ (π β π½ β (TopOnβπ)) |
14 | 1, 2, 3, 4, 5, 6, 7 | neiptopnei 22636 |
. 2
β’ (π β π = (π β π β¦ ((neiβπ½)β{π}))) |
15 | | nfv 1918 |
. . . . . . . . . 10
β’
β²π(π β§ π β (TopOnβπ)) |
16 | | nfmpt1 5257 |
. . . . . . . . . . 11
β’
β²π(π β π β¦ ((neiβπ)β{π})) |
17 | 16 | nfeq2 2921 |
. . . . . . . . . 10
β’
β²π π = (π β π β¦ ((neiβπ)β{π})) |
18 | 15, 17 | nfan 1903 |
. . . . . . . . 9
β’
β²π((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) |
19 | | nfv 1918 |
. . . . . . . . 9
β’
β²π π β π |
20 | 18, 19 | nfan 1903 |
. . . . . . . 8
β’
β²π(((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) |
21 | | simpllr 775 |
. . . . . . . . . . 11
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β π = (π β π β¦ ((neiβπ)β{π}))) |
22 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β π β π) |
23 | 22 | sselda 3983 |
. . . . . . . . . . 11
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β π β π) |
24 | | id 22 |
. . . . . . . . . . . 12
β’ (π = (π β π β¦ ((neiβπ)β{π})) β π = (π β π β¦ ((neiβπ)β{π}))) |
25 | | fvexd 6907 |
. . . . . . . . . . . 12
β’ ((π = (π β π β¦ ((neiβπ)β{π})) β§ π β π) β ((neiβπ)β{π}) β V) |
26 | 24, 25 | fvmpt2d 7012 |
. . . . . . . . . . 11
β’ ((π = (π β π β¦ ((neiβπ)β{π})) β§ π β π) β (πβπ) = ((neiβπ)β{π})) |
27 | 21, 23, 26 | syl2anc 585 |
. . . . . . . . . 10
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β (πβπ) = ((neiβπ)β{π})) |
28 | 27 | eqcomd 2739 |
. . . . . . . . 9
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β ((neiβπ)β{π}) = (πβπ)) |
29 | 28 | eleq2d 2820 |
. . . . . . . 8
β’
(((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β§ π β π) β (π β ((neiβπ)β{π}) β π β (πβπ))) |
30 | 20, 29 | ralbida 3268 |
. . . . . . 7
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β (βπ β π π β ((neiβπ)β{π}) β βπ β π π β (πβπ))) |
31 | 30 | pm5.32da 580 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β ((π β π β§ βπ β π π β ((neiβπ)β{π})) β (π β π β§ βπ β π π β (πβπ)))) |
32 | | toponss 22429 |
. . . . . . . . 9
β’ ((π β (TopOnβπ) β§ π β π) β π β π) |
33 | 32 | ad4ant24 753 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β π β π) |
34 | | topontop 22415 |
. . . . . . . . . . 11
β’ (π β (TopOnβπ) β π β Top) |
35 | 34 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β π β Top) |
36 | | opnnei 22624 |
. . . . . . . . . 10
β’ (π β Top β (π β π β βπ β π π β ((neiβπ)β{π}))) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π β βπ β π π β ((neiβπ)β{π}))) |
38 | 37 | biimpa 478 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β βπ β π π β ((neiβπ)β{π})) |
39 | 33, 38 | jca 513 |
. . . . . . 7
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ π β π) β (π β π β§ βπ β π π β ((neiβπ)β{π}))) |
40 | 37 | biimpar 479 |
. . . . . . . 8
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ βπ β π π β ((neiβπ)β{π})) β π β π) |
41 | 40 | adantrl 715 |
. . . . . . 7
β’ ((((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β§ (π β π β§ βπ β π π β ((neiβπ)β{π}))) β π β π) |
42 | 39, 41 | impbida 800 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π β (π β π β§ βπ β π π β ((neiβπ)β{π})))) |
43 | 1 | neipeltop 22633 |
. . . . . . 7
β’ (π β π½ β (π β π β§ βπ β π π β (πβπ))) |
44 | 43 | a1i 11 |
. . . . . 6
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π½ β (π β π β§ βπ β π π β (πβπ)))) |
45 | 31, 42, 44 | 3bitr4d 311 |
. . . . 5
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β (π β π β π β π½)) |
46 | 45 | eqrdv 2731 |
. . . 4
β’ (((π β§ π β (TopOnβπ)) β§ π = (π β π β¦ ((neiβπ)β{π}))) β π = π½) |
47 | 46 | ex 414 |
. . 3
β’ ((π β§ π β (TopOnβπ)) β (π = (π β π β¦ ((neiβπ)β{π})) β π = π½)) |
48 | 47 | ralrimiva 3147 |
. 2
β’ (π β βπ β (TopOnβπ)(π = (π β π β¦ ((neiβπ)β{π})) β π = π½)) |
49 | | simpl 484 |
. . . . . . 7
β’ ((π = π½ β§ π β π) β π = π½) |
50 | 49 | fveq2d 6896 |
. . . . . 6
β’ ((π = π½ β§ π β π) β (neiβπ) = (neiβπ½)) |
51 | 50 | fveq1d 6894 |
. . . . 5
β’ ((π = π½ β§ π β π) β ((neiβπ)β{π}) = ((neiβπ½)β{π})) |
52 | 51 | mpteq2dva 5249 |
. . . 4
β’ (π = π½ β (π β π β¦ ((neiβπ)β{π})) = (π β π β¦ ((neiβπ½)β{π}))) |
53 | 52 | eqeq2d 2744 |
. . 3
β’ (π = π½ β (π = (π β π β¦ ((neiβπ)β{π})) β π = (π β π β¦ ((neiβπ½)β{π})))) |
54 | 53 | eqreu 3726 |
. 2
β’ ((π½ β (TopOnβπ) β§ π = (π β π β¦ ((neiβπ½)β{π})) β§ βπ β (TopOnβπ)(π = (π β π β¦ ((neiβπ)β{π})) β π = π½)) β β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π}))) |
55 | 13, 14, 48, 54 | syl3anc 1372 |
1
β’ (π β β!π β (TopOnβπ)π = (π β π β¦ ((neiβπ)β{π}))) |