Step | Hyp | Ref
| Expression |
1 | | df-cnp 22952 |
. . 3
β’ CnP =
(π β Top, π β Top β¦ (π₯ β βͺ π
β¦ {π β (βͺ π
βm βͺ π) β£ βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))})) |
2 | 1 | a1i 11 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β CnP = (π β Top, π β Top β¦ (π₯ β βͺ π β¦ {π β (βͺ π βm βͺ π)
β£ βπ€ β
π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))}))) |
3 | | simprl 767 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = π½) |
4 | 3 | unieqd 4921 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = βͺ
π½) |
5 | | toponuni 22636 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
6 | 5 | ad2antrr 722 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = βͺ π½) |
7 | 4, 6 | eqtr4d 2773 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = π) |
8 | | simprr 769 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = πΎ) |
9 | 8 | unieqd 4921 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = βͺ
πΎ) |
10 | | toponuni 22636 |
. . . . . . 7
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
11 | 10 | ad2antlr 723 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = βͺ πΎ) |
12 | 9, 11 | eqtr4d 2773 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = π) |
13 | 12, 7 | oveq12d 7429 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (βͺ
π βm βͺ π) =
(π βm π)) |
14 | 3 | rexeqdv 3324 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (βπ£ β π (π₯ β π£ β§ (π β π£) β π€) β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))) |
15 | 14 | imbi2d 339 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€)) β ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€)))) |
16 | 8, 15 | raleqbidv 3340 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€)) β βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€)))) |
17 | 13, 16 | rabeqbidv 3447 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β {π β (βͺ π βm βͺ π)
β£ βπ€ β
π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))} = {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}) |
18 | 7, 17 | mpteq12dv 5238 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (π₯ β βͺ π β¦ {π β (βͺ π βm βͺ π)
β£ βπ€ β
π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))}) = (π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))})) |
19 | | topontop 22635 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
20 | 19 | adantr 479 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π½ β Top) |
21 | | topontop 22635 |
. . 3
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
22 | 21 | adantl 480 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β πΎ β Top) |
23 | | ovex 7444 |
. . . . . 6
β’ (π βm π) β V |
24 | | ssrab2 4076 |
. . . . . 6
β’ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β (π βm π) |
25 | 23, 24 | elpwi2 5345 |
. . . . 5
β’ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β π« (π βm π) |
26 | 25 | a1i 11 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β π) β {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β π« (π βm π)) |
27 | 26 | fmpttd 7115 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}):πβΆπ« (π βm π)) |
28 | | toponmax 22648 |
. . . 4
β’ (π½ β (TopOnβπ) β π β π½) |
29 | 28 | adantr 479 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π β π½) |
30 | 23 | pwex 5377 |
. . . 4
β’ π«
(π βm π) β V |
31 | 30 | a1i 11 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π« (π βm π) β V) |
32 | | fex2 7926 |
. . 3
β’ (((π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}):πβΆπ« (π βm π) β§ π β π½ β§ π« (π βm π) β V) β (π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}) β V) |
33 | 27, 29, 31, 32 | syl3anc 1369 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}) β V) |
34 | 2, 18, 20, 22, 33 | ovmpod 7562 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ CnP πΎ) = (π₯ β π β¦ {π β (π βm π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))})) |