Step | Hyp | Ref
| Expression |
1 | | 1stccnp.2 |
. . . . 5
β’ (π β π½ β (TopOnβπ)) |
2 | | 1stccnp.3 |
. . . . 5
β’ (π β πΎ β (TopOnβπ)) |
3 | 1, 2 | jca 513 |
. . . 4
β’ (π β (π½ β (TopOnβπ) β§ πΎ β (TopOnβπ))) |
4 | | cnpf2 22617 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
5 | 4 | 3expa 1119 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
6 | 3, 5 | sylan 581 |
. . 3
β’ ((π β§ πΉ β ((π½ CnP πΎ)βπ)) β πΉ:πβΆπ) |
7 | | simprr 772 |
. . . . . 6
β’ (((π β§ πΉ β ((π½ CnP πΎ)βπ)) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β π(βπ‘βπ½)π) |
8 | | simplr 768 |
. . . . . 6
β’ (((π β§ πΉ β ((π½ CnP πΎ)βπ)) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β πΉ β ((π½ CnP πΎ)βπ)) |
9 | 7, 8 | lmcnp 22671 |
. . . . 5
β’ (((π β§ πΉ β ((π½ CnP πΎ)βπ)) β§ (π:ββΆπ β§ π(βπ‘βπ½)π)) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) |
10 | 9 | ex 414 |
. . . 4
β’ ((π β§ πΉ β ((π½ CnP πΎ)βπ)) β ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ))) |
11 | 10 | alrimiv 1931 |
. . 3
β’ ((π β§ πΉ β ((π½ CnP πΎ)βπ)) β βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ))) |
12 | 6, 11 | jca 513 |
. 2
β’ ((π β§ πΉ β ((π½ CnP πΎ)βπ)) β (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) |
13 | | simprl 770 |
. . 3
β’ ((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β πΉ:πβΆπ) |
14 | | fal 1556 |
. . . . . . . . 9
β’ Β¬
β₯ |
15 | | 19.29 1877 |
. . . . . . . . . . . . . 14
β’
((βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β§ βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β βπ(((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π))) |
16 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β π:ββΆ(π β (β‘πΉ β π’))) |
17 | | difss 4092 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (β‘πΉ β π’)) β π |
18 | | fss 6686 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π:ββΆ(π β (β‘πΉ β π’)) β§ (π β (β‘πΉ β π’)) β π) β π:ββΆπ) |
19 | 16, 17, 18 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β π:ββΆπ) |
20 | | simprr 772 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β π(βπ‘βπ½)π) |
21 | 19, 20 | jca 513 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β (π:ββΆπ β§ π(βπ‘βπ½)π)) |
22 | | nnuz 12811 |
. . . . . . . . . . . . . . . . . . . . 21
β’ β =
(β€β₯β1) |
23 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β (πΉβπ) β π’) |
24 | | 1zzd 12539 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β 1 β
β€) |
25 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) |
26 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β π’ β πΎ) |
27 | 22, 23, 24, 25, 26 | lmcvg 22629 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β βπ β β βπ β (β€β₯βπ)((πΉ β π)βπ) β π’) |
28 | 22 | r19.2uz 15242 |
. . . . . . . . . . . . . . . . . . . . 21
β’
(βπ β
β βπ β
(β€β₯βπ)((πΉ β π)βπ) β π’ β βπ β β ((πΉ β π)βπ) β π’) |
29 | | simprll 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β π:ββΆ(π β (β‘πΉ β π’))) |
30 | 29 | ffnd 6670 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β π Fn β) |
31 | | fvco2 6939 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π Fn β β§ π β β) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
32 | 30, 31 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β ((πΉ β π)βπ) = (πΉβ(πβπ))) |
33 | 32 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β (((πΉ β π)βπ) β π’ β (πΉβ(πβπ)) β π’)) |
34 | 29 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β (πβπ) β (π β (β‘πΉ β π’))) |
35 | 34 | eldifad 3923 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β (πβπ) β π) |
36 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β πΉ:πβΆπ) |
37 | 36 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β πΉ:πβΆπ) |
38 | | ffn 6669 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΉ:πβΆπ β πΉ Fn π) |
39 | | elpreima 7009 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΉ Fn π β ((πβπ) β (β‘πΉ β π’) β ((πβπ) β π β§ (πΉβ(πβπ)) β π’))) |
40 | 37, 38, 39 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β ((πβπ) β (β‘πΉ β π’) β ((πβπ) β π β§ (πΉβ(πβπ)) β π’))) |
41 | 34 | eldifbd 3924 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β Β¬ (πβπ) β (β‘πΉ β π’)) |
42 | 41 | pm2.21d 121 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β ((πβπ) β (β‘πΉ β π’) β β₯)) |
43 | 40, 42 | sylbird 260 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β (((πβπ) β π β§ (πΉβ(πβπ)) β π’) β β₯)) |
44 | 35, 43 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β ((πΉβ(πβπ)) β π’ β β₯)) |
45 | 33, 44 | sylbid 239 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β§ π β β) β (((πΉ β π)βπ) β π’ β β₯)) |
46 | 45 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β (βπ β β ((πΉ β π)βπ) β π’ β β₯)) |
47 | 28, 46 | syl5 34 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β (βπ β β βπ β (β€β₯βπ)((πΉ β π)βπ) β π’ β β₯)) |
48 | 27, 47 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β§ (πΉ β π)(βπ‘βπΎ)(πΉβπ))) β β₯) |
49 | 48 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β ((πΉ β π)(βπ‘βπΎ)(πΉβπ) β β₯)) |
50 | 21, 49 | embantd 59 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β (((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β β₯)) |
51 | 50 | ex 414 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β ((π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β (((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β β₯))) |
52 | 51 | impcomd 413 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β ((((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β β₯)) |
53 | 52 | exlimdv 1937 |
. . . . . . . . . . . . . 14
β’ (((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (βπ(((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β§ (π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β β₯)) |
54 | 15, 53 | syl5 34 |
. . . . . . . . . . . . 13
β’ (((π β§ πΉ:πβΆπ) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β ((βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β§ βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) β β₯)) |
55 | 54 | exp4b 432 |
. . . . . . . . . . . 12
β’ ((π β§ πΉ:πβΆπ) β ((π’ β πΎ β§ (πΉβπ) β π’) β (βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β (βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β β₯)))) |
56 | 55 | com23 86 |
. . . . . . . . . . 11
β’ ((π β§ πΉ:πβΆπ) β (βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)) β ((π’ β πΎ β§ (πΉβπ) β π’) β (βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β β₯)))) |
57 | 56 | impr 456 |
. . . . . . . . . 10
β’ ((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β ((π’ β πΎ β§ (πΉβπ) β π’) β (βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β β₯))) |
58 | 57 | imp 408 |
. . . . . . . . 9
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π) β β₯)) |
59 | 14, 58 | mtoi 198 |
. . . . . . . 8
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β Β¬ βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π)) |
60 | | 1stccnp.1 |
. . . . . . . . . 10
β’ (π β π½ β
1stΟ) |
61 | 60 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β π½ β
1stΟ) |
62 | 1 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β π½ β (TopOnβπ)) |
63 | | toponuni 22279 |
. . . . . . . . . . 11
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β π = βͺ π½) |
65 | 17, 64 | sseqtrid 3997 |
. . . . . . . . 9
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (π β (β‘πΉ β π’)) β βͺ π½) |
66 | | eqid 2733 |
. . . . . . . . . 10
β’ βͺ π½ =
βͺ π½ |
67 | 66 | 1stcelcls 22828 |
. . . . . . . . 9
β’ ((π½ β 1stΟ
β§ (π β (β‘πΉ β π’)) β βͺ π½) β (π β ((clsβπ½)β(π β (β‘πΉ β π’))) β βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π))) |
68 | 61, 65, 67 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (π β ((clsβπ½)β(π β (β‘πΉ β π’))) β βπ(π:ββΆ(π β (β‘πΉ β π’)) β§ π(βπ‘βπ½)π))) |
69 | 59, 68 | mtbird 325 |
. . . . . . 7
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β Β¬ π β ((clsβπ½)β(π β (β‘πΉ β π’)))) |
70 | | topontop 22278 |
. . . . . . . . 9
β’ (π½ β (TopOnβπ) β π½ β Top) |
71 | 62, 70 | syl 17 |
. . . . . . . 8
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β π½ β Top) |
72 | | 1stccnp.4 |
. . . . . . . . . 10
β’ (π β π β π) |
73 | 72 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β π β π) |
74 | 73, 64 | eleqtrd 2836 |
. . . . . . . 8
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β π β βͺ π½) |
75 | 66 | elcls 22440 |
. . . . . . . 8
β’ ((π½ β Top β§ (π β (β‘πΉ β π’)) β βͺ π½ β§ π β βͺ π½) β (π β ((clsβπ½)β(π β (β‘πΉ β π’))) β βπ£ β π½ (π β π£ β (π£ β© (π β (β‘πΉ β π’))) β β
))) |
76 | 71, 65, 74, 75 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (π β ((clsβπ½)β(π β (β‘πΉ β π’))) β βπ£ β π½ (π β π£ β (π£ β© (π β (β‘πΉ β π’))) β β
))) |
77 | 69, 76 | mtbid 324 |
. . . . . 6
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β Β¬ βπ£ β π½ (π β π£ β (π£ β© (π β (β‘πΉ β π’))) β β
)) |
78 | 13 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β πΉ:πβΆπ) |
79 | 78 | ffund 6673 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β Fun πΉ) |
80 | | toponss 22292 |
. . . . . . . . . . . . . 14
β’ ((π½ β (TopOnβπ) β§ π£ β π½) β π£ β π) |
81 | 62, 80 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β π£ β π) |
82 | 78 | fdmd 6680 |
. . . . . . . . . . . . 13
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β dom πΉ = π) |
83 | 81, 82 | sseqtrrd 3986 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β π£ β dom πΉ) |
84 | | funimass3 7005 |
. . . . . . . . . . . 12
β’ ((Fun
πΉ β§ π£ β dom πΉ) β ((πΉ β π£) β π’ β π£ β (β‘πΉ β π’))) |
85 | 79, 83, 84 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β ((πΉ β π£) β π’ β π£ β (β‘πΉ β π’))) |
86 | | df-ss 3928 |
. . . . . . . . . . . . 13
β’ (π£ β π β (π£ β© π) = π£) |
87 | 81, 86 | sylib 217 |
. . . . . . . . . . . 12
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β (π£ β© π) = π£) |
88 | 87 | sseq1d 3976 |
. . . . . . . . . . 11
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β ((π£ β© π) β (β‘πΉ β π’) β π£ β (β‘πΉ β π’))) |
89 | 85, 88 | bitr4d 282 |
. . . . . . . . . 10
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β ((πΉ β π£) β π’ β (π£ β© π) β (β‘πΉ β π’))) |
90 | | nne 2944 |
. . . . . . . . . . 11
β’ (Β¬
(π£ β© (π β (β‘πΉ β π’))) β β
β (π£ β© (π β (β‘πΉ β π’))) = β
) |
91 | | inssdif0 4330 |
. . . . . . . . . . 11
β’ ((π£ β© π) β (β‘πΉ β π’) β (π£ β© (π β (β‘πΉ β π’))) = β
) |
92 | 90, 91 | bitr4i 278 |
. . . . . . . . . 10
β’ (Β¬
(π£ β© (π β (β‘πΉ β π’))) β β
β (π£ β© π) β (β‘πΉ β π’)) |
93 | 89, 92 | bitr4di 289 |
. . . . . . . . 9
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β ((πΉ β π£) β π’ β Β¬ (π£ β© (π β (β‘πΉ β π’))) β β
)) |
94 | 93 | anbi2d 630 |
. . . . . . . 8
β’ ((((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β§ π£ β π½) β ((π β π£ β§ (πΉ β π£) β π’) β (π β π£ β§ Β¬ (π£ β© (π β (β‘πΉ β π’))) β β
))) |
95 | 94 | rexbidva 3170 |
. . . . . . 7
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’) β βπ£ β π½ (π β π£ β§ Β¬ (π£ β© (π β (β‘πΉ β π’))) β β
))) |
96 | | rexanali 3102 |
. . . . . . 7
β’
(βπ£ β
π½ (π β π£ β§ Β¬ (π£ β© (π β (β‘πΉ β π’))) β β
) β Β¬ βπ£ β π½ (π β π£ β (π£ β© (π β (β‘πΉ β π’))) β β
)) |
97 | 95, 96 | bitrdi 287 |
. . . . . 6
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β (βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’) β Β¬ βπ£ β π½ (π β π£ β (π£ β© (π β (β‘πΉ β π’))) β β
))) |
98 | 77, 97 | mpbird 257 |
. . . . 5
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ (π’ β πΎ β§ (πΉβπ) β π’)) β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’)) |
99 | 98 | expr 458 |
. . . 4
β’ (((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β§ π’ β πΎ) β ((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
100 | 99 | ralrimiva 3140 |
. . 3
β’ ((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β βπ’ β πΎ ((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))) |
101 | | iscnp 22604 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))))) |
102 | 1, 2, 72, 101 | syl3anc 1372 |
. . . 4
β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))))) |
103 | 102 | adantr 482 |
. . 3
β’ ((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ’ β πΎ ((πΉβπ) β π’ β βπ£ β π½ (π β π£ β§ (πΉ β π£) β π’))))) |
104 | 13, 100, 103 | mpbir2and 712 |
. 2
β’ ((π β§ (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ)))) β πΉ β ((π½ CnP πΎ)βπ)) |
105 | 12, 104 | impbida 800 |
1
β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ))))) |