Step | Hyp | Ref
| Expression |
1 | | topontop 13517 |
. . . . . . 7
β’ (π½ β (TopOnβπ) β π½ β Top) |
2 | 1 | 3ad2ant1 1018 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β π½ β Top) |
3 | | simp2 998 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β πΎ β Top) |
4 | | uniexg 4440 |
. . . . . . . 8
β’ (π½ β (TopOnβπ) β βͺ π½
β V) |
5 | 4 | 3ad2ant1 1018 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β βͺ π½ β V) |
6 | | mptexg 5742 |
. . . . . . 7
β’ (βͺ π½
β V β (π₯ β
βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) β V) |
7 | 5, 6 | syl 14 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) β V) |
8 | | unieq 3819 |
. . . . . . . 8
β’ (π = π½ β βͺ π = βͺ
π½) |
9 | 8 | oveq2d 5891 |
. . . . . . . . 9
β’ (π = π½ β (βͺ π βπ
βͺ π) = (βͺ π βπ
βͺ π½)) |
10 | | rexeq 2674 |
. . . . . . . . . . 11
β’ (π = π½ β (βπ β π (π₯ β π β§ (π β π) β π¦) β βπ β π½ (π₯ β π β§ (π β π) β π¦))) |
11 | 10 | imbi2d 230 |
. . . . . . . . . 10
β’ (π = π½ β (((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦)) β ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦)))) |
12 | 11 | ralbidv 2477 |
. . . . . . . . 9
β’ (π = π½ β (βπ¦ β π ((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦)) β βπ¦ β π ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦)))) |
13 | 9, 12 | rabeqbidv 2733 |
. . . . . . . 8
β’ (π = π½ β {π β (βͺ π βπ
βͺ π) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦))} = {π β (βͺ π βπ
βͺ π½) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) |
14 | 8, 13 | mpteq12dv 4086 |
. . . . . . 7
β’ (π = π½ β (π₯ β βͺ π β¦ {π β (βͺ π βπ
βͺ π) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦))}) = (π₯ β βͺ π½ β¦ {π β (βͺ π βπ
βͺ π½) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))})) |
15 | | unieq 3819 |
. . . . . . . . . 10
β’ (π = πΎ β βͺ π = βͺ
πΎ) |
16 | 15 | oveq1d 5890 |
. . . . . . . . 9
β’ (π = πΎ β (βͺ π βπ
βͺ π½) = (βͺ πΎ βπ
βͺ π½)) |
17 | | raleq 2673 |
. . . . . . . . 9
β’ (π = πΎ β (βπ¦ β π ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦)) β βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦)))) |
18 | 16, 17 | rabeqbidv 2733 |
. . . . . . . 8
β’ (π = πΎ β {π β (βͺ π βπ
βͺ π½) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))} = {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) |
19 | 18 | mpteq2dv 4095 |
. . . . . . 7
β’ (π = πΎ β (π₯ β βͺ π½ β¦ {π β (βͺ π βπ
βͺ π½) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) = (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))})) |
20 | | df-cnp 13692 |
. . . . . . 7
β’ CnP =
(π β Top, π β Top β¦ (π₯ β βͺ π
β¦ {π β (βͺ π
βπ βͺ π) β£ βπ¦ β π ((πβπ₯) β π¦ β βπ β π (π₯ β π β§ (π β π) β π¦))})) |
21 | 14, 19, 20 | ovmpog 6009 |
. . . . . 6
β’ ((π½ β Top β§ πΎ β Top β§ (π₯ β βͺ π½
β¦ {π β (βͺ πΎ
βπ βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) β V) β (π½ CnP πΎ) = (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))})) |
22 | 2, 3, 7, 21 | syl3anc 1238 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β (π½ CnP πΎ) = (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))})) |
23 | 22 | dmeqd 4830 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β dom (π½ CnP πΎ) = dom (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))})) |
24 | | eqid 2177 |
. . . . 5
β’ (π₯ β βͺ π½
β¦ {π β (βͺ πΎ
βπ βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) = (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) |
25 | 24 | dmmptss 5126 |
. . . 4
β’ dom
(π₯ β βͺ π½
β¦ {π β (βͺ πΎ
βπ βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) β βͺ
π½ |
26 | 23, 25 | eqsstrdi 3208 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β dom (π½ CnP πΎ) β βͺ π½) |
27 | | toponuni 13518 |
. . . 4
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
28 | 27 | 3ad2ant1 1018 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β π = βͺ π½) |
29 | 26, 28 | sseqtrrd 3195 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β dom (π½ CnP πΎ) β π) |
30 | | mptrel 4756 |
. . . 4
β’ Rel
(π₯ β βͺ π½
β¦ {π β (βͺ πΎ
βπ βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}) |
31 | 22 | releqd 4711 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β (Rel (π½ CnP πΎ) β Rel (π₯ β βͺ π½ β¦ {π β (βͺ πΎ βπ
βͺ π½) β£ βπ¦ β πΎ ((πβπ₯) β π¦ β βπ β π½ (π₯ β π β§ (π β π) β π¦))}))) |
32 | 30, 31 | mpbiri 168 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β Rel (π½ CnP πΎ)) |
33 | | simp3 999 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ β ((π½ CnP πΎ)βπ)) |
34 | | relelfvdm 5548 |
. . 3
β’ ((Rel
(π½ CnP πΎ) β§ πΉ β ((π½ CnP πΎ)βπ)) β π β dom (π½ CnP πΎ)) |
35 | 32, 33, 34 | syl2anc 411 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β π β dom (π½ CnP πΎ)) |
36 | 29, 35 | sseldd 3157 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β Top β§ πΉ β ((π½ CnP πΎ)βπ)) β π β π) |