Step | Hyp | Ref
| Expression |
1 | | fconst6g 6751 |
. . 3
β’ (π΅ β π β (π Γ {π΅}):πβΆπ) |
2 | 1 | 3ad2ant3 1135 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}):πβΆπ) |
3 | 2 | adantr 481 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β (π Γ {π΅}):πβΆπ) |
4 | | simpll3 1214 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ π¦ β πΎ) β π΅ β π) |
5 | | simplr 767 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ π¦ β πΎ) β π₯ β π) |
6 | | fvconst2g 7171 |
. . . . . . . 8
β’ ((π΅ β π β§ π₯ β π) β ((π Γ {π΅})βπ₯) = π΅) |
7 | 4, 5, 6 | syl2anc 584 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ π¦ β πΎ) β ((π Γ {π΅})βπ₯) = π΅) |
8 | 7 | eleq1d 2817 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ π¦ β πΎ) β (((π Γ {π΅})βπ₯) β π¦ β π΅ β π¦)) |
9 | | simpll1 1212 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β π½ β (TopOnβπ)) |
10 | | toponmax 22327 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π β π½) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β π β π½) |
12 | | simplr 767 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β π₯ β π) |
13 | | df-ima 5666 |
. . . . . . . . 9
β’ ((π Γ {π΅}) β π) = ran ((π Γ {π΅}) βΎ π) |
14 | | ssid 3984 |
. . . . . . . . . . . . 13
β’ π β π |
15 | | xpssres 5994 |
. . . . . . . . . . . . 13
β’ (π β π β ((π Γ {π΅}) βΎ π) = (π Γ {π΅})) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((π Γ {π΅}) βΎ π) = (π Γ {π΅}) |
17 | 16 | rneqi 5912 |
. . . . . . . . . . 11
β’ ran
((π Γ {π΅}) βΎ π) = ran (π Γ {π΅}) |
18 | | rnxpss 6144 |
. . . . . . . . . . 11
β’ ran
(π Γ {π΅}) β {π΅} |
19 | 17, 18 | eqsstri 3996 |
. . . . . . . . . 10
β’ ran
((π Γ {π΅}) βΎ π) β {π΅} |
20 | | simprr 771 |
. . . . . . . . . . 11
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β π΅ β π¦) |
21 | 20 | snssd 4789 |
. . . . . . . . . 10
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β {π΅} β π¦) |
22 | 19, 21 | sstrid 3973 |
. . . . . . . . 9
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β ran ((π Γ {π΅}) βΎ π) β π¦) |
23 | 13, 22 | eqsstrid 4010 |
. . . . . . . 8
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β ((π Γ {π΅}) β π) β π¦) |
24 | | eleq2 2821 |
. . . . . . . . . 10
β’ (π’ = π β (π₯ β π’ β π₯ β π)) |
25 | | imaeq2 6029 |
. . . . . . . . . . 11
β’ (π’ = π β ((π Γ {π΅}) β π’) = ((π Γ {π΅}) β π)) |
26 | 25 | sseq1d 3993 |
. . . . . . . . . 10
β’ (π’ = π β (((π Γ {π΅}) β π’) β π¦ β ((π Γ {π΅}) β π) β π¦)) |
27 | 24, 26 | anbi12d 631 |
. . . . . . . . 9
β’ (π’ = π β ((π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦) β (π₯ β π β§ ((π Γ {π΅}) β π) β π¦))) |
28 | 27 | rspcev 3595 |
. . . . . . . 8
β’ ((π β π½ β§ (π₯ β π β§ ((π Γ {π΅}) β π) β π¦)) β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦)) |
29 | 11, 12, 23, 28 | syl12anc 835 |
. . . . . . 7
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ (π¦ β πΎ β§ π΅ β π¦)) β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦)) |
30 | 29 | expr 457 |
. . . . . 6
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ π¦ β πΎ) β (π΅ β π¦ β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦))) |
31 | 8, 30 | sylbid 239 |
. . . . 5
β’ ((((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β§ π¦ β πΎ) β (((π Γ {π΅})βπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦))) |
32 | 31 | ralrimiva 3145 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β βπ¦ β πΎ (((π Γ {π΅})βπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦))) |
33 | | simpl1 1191 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β π½ β (TopOnβπ)) |
34 | | simpl2 1192 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β πΎ β (TopOnβπ)) |
35 | | simpr 485 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β π₯ β π) |
36 | | iscnp 22640 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π₯ β π) β ((π Γ {π΅}) β ((π½ CnP πΎ)βπ₯) β ((π Γ {π΅}):πβΆπ β§ βπ¦ β πΎ (((π Γ {π΅})βπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦))))) |
37 | 33, 34, 35, 36 | syl3anc 1371 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β ((π Γ {π΅}) β ((π½ CnP πΎ)βπ₯) β ((π Γ {π΅}):πβΆπ β§ βπ¦ β πΎ (((π Γ {π΅})βπ₯) β π¦ β βπ’ β π½ (π₯ β π’ β§ ((π Γ {π΅}) β π’) β π¦))))) |
38 | 3, 32, 37 | mpbir2and 711 |
. . 3
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β§ π₯ β π) β (π Γ {π΅}) β ((π½ CnP πΎ)βπ₯)) |
39 | 38 | ralrimiva 3145 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β βπ₯ β π (π Γ {π΅}) β ((π½ CnP πΎ)βπ₯)) |
40 | | cncnp 22683 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β ((π Γ {π΅}) β (π½ Cn πΎ) β ((π Γ {π΅}):πβΆπ β§ βπ₯ β π (π Γ {π΅}) β ((π½ CnP πΎ)βπ₯)))) |
41 | 40 | 3adant3 1132 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β ((π Γ {π΅}) β (π½ Cn πΎ) β ((π Γ {π΅}):πβΆπ β§ βπ₯ β π (π Γ {π΅}) β ((π½ CnP πΎ)βπ₯)))) |
42 | 2, 39, 41 | mpbir2and 711 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΅ β π) β (π Γ {π΅}) β (π½ Cn πΎ)) |