Step | Hyp | Ref
| Expression |
1 | | df-cnp 13774 |
. . 3
β’ CnP =
(π β Top, π β Top β¦ (π₯ β βͺ π
β¦ {π β (βͺ π
βπ βͺ π) β£ βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))})) |
2 | 1 | a1i 9 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β CnP = (π β Top, π β Top β¦ (π₯ β βͺ π β¦ {π β (βͺ π βπ
βͺ π) β£ βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))}))) |
3 | | simprl 529 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = π½) |
4 | 3 | unieqd 3822 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = βͺ
π½) |
5 | | toponuni 13600 |
. . . . 5
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
6 | 5 | ad2antrr 488 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = βͺ π½) |
7 | 4, 6 | eqtr4d 2213 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = π) |
8 | | simprr 531 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = πΎ) |
9 | 8 | unieqd 3822 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = βͺ
πΎ) |
10 | | toponuni 13600 |
. . . . . . 7
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
11 | 10 | ad2antlr 489 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β π = βͺ πΎ) |
12 | 9, 11 | eqtr4d 2213 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β βͺ π = π) |
13 | 12, 7 | oveq12d 5895 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (βͺ
π
βπ βͺ π) = (π βπ π)) |
14 | 3 | rexeqdv 2680 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (βπ£ β π (π₯ β π£ β§ (π β π£) β π€) β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))) |
15 | 14 | imbi2d 230 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€)) β ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€)))) |
16 | 8, 15 | raleqbidv 2685 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€)) β βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€)))) |
17 | 13, 16 | rabeqbidv 2734 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β {π β (βͺ π βπ
βͺ π) β£ βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))} = {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}) |
18 | 7, 17 | mpteq12dv 4087 |
. 2
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (π = π½ β§ π = πΎ)) β (π₯ β βͺ π β¦ {π β (βͺ π βπ
βͺ π) β£ βπ€ β π ((πβπ₯) β π€ β βπ£ β π (π₯ β π£ β§ (π β π£) β π€))}) = (π₯ β π β¦ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))})) |
19 | | topontop 13599 |
. . 3
β’ (π½ β (TopOnβπ) β π½ β Top) |
20 | 19 | adantr 276 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π½ β Top) |
21 | | topontop 13599 |
. . 3
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
22 | 21 | adantl 277 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β πΎ β Top) |
23 | | fnmap 6657 |
. . . . . . . 8
β’
βπ Fn (V Γ V) |
24 | 23 | a1i 9 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β βπ Fn (V
Γ V)) |
25 | | toponmax 13610 |
. . . . . . . . 9
β’ (πΎ β (TopOnβπ) β π β πΎ) |
26 | 25 | elexd 2752 |
. . . . . . . 8
β’ (πΎ β (TopOnβπ) β π β V) |
27 | 26 | adantl 277 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π β V) |
28 | | toponmax 13610 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π β π½) |
29 | 28 | elexd 2752 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β π β V) |
30 | 29 | adantr 276 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π β V) |
31 | | fnovex 5910 |
. . . . . . 7
β’ ((
βπ Fn (V Γ V) β§ π β V β§ π β V) β (π βπ π) β V) |
32 | 24, 27, 30, 31 | syl3anc 1238 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π βπ π) β V) |
33 | 32 | adantr 276 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β π) β (π βπ π) β V) |
34 | | ssrab2 3242 |
. . . . . 6
β’ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β (π βπ π) |
35 | | elpw2g 4158 |
. . . . . 6
β’ ((π βπ
π) β V β ({π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β π« (π βπ π) β {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β (π βπ π))) |
36 | 34, 35 | mpbiri 168 |
. . . . 5
β’ ((π βπ
π) β V β {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β π« (π βπ π)) |
37 | 33, 36 | syl 14 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β π) β {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))} β π« (π βπ π)) |
38 | 37 | fmpttd 5673 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π₯ β π β¦ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}):πβΆπ« (π βπ π)) |
39 | 28 | adantr 276 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π β π½) |
40 | 32 | pwexd 4183 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β π« (π βπ π) β V) |
41 | | fex2 5386 |
. . 3
β’ (((π₯ β π β¦ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}):πβΆπ« (π βπ π) β§ π β π½ β§ π« (π βπ π) β V) β (π₯ β π β¦ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}) β V) |
42 | 38, 39, 40, 41 | syl3anc 1238 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π₯ β π β¦ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))}) β V) |
43 | 2, 18, 20, 22, 42 | ovmpod 6004 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ CnP πΎ) = (π₯ β π β¦ {π β (π βπ π) β£ βπ€ β πΎ ((πβπ₯) β π€ β βπ£ β π½ (π₯ β π£ β§ (π β π£) β π€))})) |