Step | Hyp | Ref
| Expression |
1 | | cnvimass 4992 |
. . . . . . . 8
β’ (β‘πΉ β π¦) β dom πΉ |
2 | | fdm 5372 |
. . . . . . . 8
β’ (πΉ:πβΆπ β dom πΉ = π) |
3 | 1, 2 | sseqtrid 3206 |
. . . . . . 7
β’ (πΉ:πβΆπ β (β‘πΉ β π¦) β π) |
4 | 3 | 3ad2ant3 1020 |
. . . . . 6
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (β‘πΉ β π¦) β π) |
5 | 4 | ad2antrr 488 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β (β‘πΉ β π¦) β π) |
6 | | neii2 13652 |
. . . . . . . 8
β’ ((πΎ β Top β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β βπ β πΎ ({(πΉβπ΄)} β π β§ π β π¦)) |
7 | 6 | 3ad2antl2 1160 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β βπ β πΎ ({(πΉβπ΄)} β π β§ π β π¦)) |
8 | 7 | ad2ant2rl 511 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β βπ β πΎ ({(πΉβπ΄)} β π β§ π β π¦)) |
9 | | cnpnei.1 |
. . . . . . . . . . . 12
β’ π = βͺ
π½ |
10 | 9 | toptopon 13521 |
. . . . . . . . . . 11
β’ (π½ β Top β π½ β (TopOnβπ)) |
11 | 10 | biimpi 120 |
. . . . . . . . . 10
β’ (π½ β Top β π½ β (TopOnβπ)) |
12 | 11 | 3ad2ant1 1018 |
. . . . . . . . 9
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β π½ β (TopOnβπ)) |
13 | 12 | ad3antrrr 492 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β π½ β (TopOnβπ)) |
14 | | cnpnei.2 |
. . . . . . . . . . . 12
β’ π = βͺ
πΎ |
15 | 14 | toptopon 13521 |
. . . . . . . . . . 11
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
16 | 15 | biimpi 120 |
. . . . . . . . . 10
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
17 | 16 | 3ad2ant2 1019 |
. . . . . . . . 9
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β πΎ β (TopOnβπ)) |
18 | 17 | ad3antrrr 492 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β πΎ β (TopOnβπ)) |
19 | | simpllr 534 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β π΄ β π) |
20 | | simplrl 535 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β πΉ β ((π½ CnP πΎ)βπ΄)) |
21 | | simprl 529 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β π β πΎ) |
22 | | simprrl 539 |
. . . . . . . . 9
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β {(πΉβπ΄)} β π) |
23 | | fvexg 5535 |
. . . . . . . . . . 11
β’ ((πΉ β ((π½ CnP πΎ)βπ΄) β§ π΄ β π) β (πΉβπ΄) β V) |
24 | 20, 19, 23 | syl2anc 411 |
. . . . . . . . . 10
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (πΉβπ΄) β V) |
25 | | snssg 3727 |
. . . . . . . . . 10
β’ ((πΉβπ΄) β V β ((πΉβπ΄) β π β {(πΉβπ΄)} β π)) |
26 | 24, 25 | syl 14 |
. . . . . . . . 9
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β ((πΉβπ΄) β π β {(πΉβπ΄)} β π)) |
27 | 22, 26 | mpbird 167 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (πΉβπ΄) β π) |
28 | | icnpimaex 13714 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π β πΎ β§ (πΉβπ΄) β π)) β βπ β π½ (π΄ β π β§ (πΉ β π) β π)) |
29 | 13, 18, 19, 20, 21, 27, 28 | syl33anc 1253 |
. . . . . . 7
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β βπ β π½ (π΄ β π β§ (πΉ β π) β π)) |
30 | | sstr2 3163 |
. . . . . . . . . . . . 13
β’ ((πΉ β π) β π β (π β π¦ β (πΉ β π) β π¦)) |
31 | 30 | com12 30 |
. . . . . . . . . . . 12
β’ (π β π¦ β ((πΉ β π) β π β (πΉ β π) β π¦)) |
32 | 31 | ad2antll 491 |
. . . . . . . . . . 11
β’ ((π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦)) β ((πΉ β π) β π β (πΉ β π) β π¦)) |
33 | 32 | ad2antlr 489 |
. . . . . . . . . 10
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((πΉ β π) β π β (πΉ β π) β π¦)) |
34 | | ffun 5369 |
. . . . . . . . . . . . . 14
β’ (πΉ:πβΆπ β Fun πΉ) |
35 | 34 | 3ad2ant3 1020 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β Fun πΉ) |
36 | 35 | ad2antrr 488 |
. . . . . . . . . . . 12
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β Fun πΉ) |
37 | 36 | ad2antrr 488 |
. . . . . . . . . . 11
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β Fun πΉ) |
38 | 9 | eltopss 13512 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π β π½) β π β π) |
39 | 38 | adantlr 477 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β π) |
40 | 2 | sseq2d 3186 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πβΆπ β (π β dom πΉ β π β π)) |
41 | 40 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β Top β§ πΉ:πβΆπ) β§ π β π½) β (π β dom πΉ β π β π)) |
42 | 39, 41 | mpbird 167 |
. . . . . . . . . . . . . . 15
β’ (((π½ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β dom πΉ) |
43 | 42 | 3adantl2 1154 |
. . . . . . . . . . . . . 14
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β dom πΉ) |
44 | 43 | adantlr 477 |
. . . . . . . . . . . . 13
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β π β dom πΉ) |
45 | 44 | adantlr 477 |
. . . . . . . . . . . 12
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ π β π½) β π β dom πΉ) |
46 | 45 | adantlr 477 |
. . . . . . . . . . 11
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β π β dom πΉ) |
47 | | funimass3 5633 |
. . . . . . . . . . 11
β’ ((Fun
πΉ β§ π β dom πΉ) β ((πΉ β π) β π¦ β π β (β‘πΉ β π¦))) |
48 | 37, 46, 47 | syl2anc 411 |
. . . . . . . . . 10
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((πΉ β π) β π¦ β π β (β‘πΉ β π¦))) |
49 | 33, 48 | sylibd 149 |
. . . . . . . . 9
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((πΉ β π) β π β π β (β‘πΉ β π¦))) |
50 | 49 | anim2d 337 |
. . . . . . . 8
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((π΄ β π β§ (πΉ β π) β π) β (π΄ β π β§ π β (β‘πΉ β π¦)))) |
51 | 50 | reximdva 2579 |
. . . . . . 7
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (βπ β π½ (π΄ β π β§ (πΉ β π) β π) β βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦)))) |
52 | 29, 51 | mpd 13 |
. . . . . 6
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))) |
53 | 8, 52 | rexlimddv 2599 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))) |
54 | 9 | isneip 13649 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β π) β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β ((β‘πΉ β π¦) β π β§ βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))))) |
55 | 54 | 3ad2antl1 1159 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β ((β‘πΉ β π¦) β π β§ βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))))) |
56 | 55 | adantr 276 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β ((β‘πΉ β π¦) β π β§ βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))))) |
57 | 5, 53, 56 | mpbir2and 944 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β (β‘πΉ β π¦) β ((neiβπ½)β{π΄})) |
58 | 57 | exp32 365 |
. . 3
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π¦ β ((neiβπΎ)β{(πΉβπ΄)}) β (β‘πΉ β π¦) β ((neiβπ½)β{π΄})))) |
59 | 58 | ralrimdv 2556 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}))) |
60 | | simpll3 1038 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β πΉ:πβΆπ) |
61 | | opnneip 13662 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Top β§ π β πΎ β§ (πΉβπ΄) β π) β π β ((neiβπΎ)β{(πΉβπ΄)})) |
62 | | imaeq2 4967 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (β‘πΉ β π¦) = (β‘πΉ β π)) |
63 | 62 | eleq1d 2246 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
64 | 63 | rspcv 2838 |
. . . . . . . . . . . . . 14
β’ (π β ((neiβπΎ)β{(πΉβπ΄)}) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
65 | 61, 64 | syl 14 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ π β πΎ β§ (πΉβπ΄) β π) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
66 | 65 | 3com23 1209 |
. . . . . . . . . . . 12
β’ ((πΎ β Top β§ (πΉβπ΄) β π β§ π β πΎ) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
67 | 66 | 3expb 1204 |
. . . . . . . . . . 11
β’ ((πΎ β Top β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
68 | 67 | 3ad2antl2 1160 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
69 | 68 | adantlr 477 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
70 | | neii2 13652 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ (β‘πΉ β π) β ((neiβπ½)β{π΄})) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π))) |
71 | 70 | ex 115 |
. . . . . . . . . . 11
β’ (π½ β Top β ((β‘πΉ β π) β ((neiβπ½)β{π΄}) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)))) |
72 | 71 | 3ad2ant1 1018 |
. . . . . . . . . 10
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β ((β‘πΉ β π) β ((neiβπ½)β{π΄}) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)))) |
73 | 72 | ad2antrr 488 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β ((β‘πΉ β π) β ((neiβπ½)β{π΄}) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)))) |
74 | | snssg 3727 |
. . . . . . . . . . . . 13
β’ (π΄ β π β (π΄ β π β {π΄} β π)) |
75 | 74 | ad3antlr 493 |
. . . . . . . . . . . 12
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β (π΄ β π β {π΄} β π)) |
76 | 35 | ad3antrrr 492 |
. . . . . . . . . . . . 13
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β Fun πΉ) |
77 | 9 | eltopss 13512 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ π β π½) β π β π) |
78 | 77 | 3ad2antl1 1159 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β π) |
79 | 2 | sseq2d 3186 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ:πβΆπ β (π β dom πΉ β π β π)) |
80 | 79 | 3ad2ant3 1020 |
. . . . . . . . . . . . . . . . 17
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (π β dom πΉ β π β π)) |
81 | 80 | biimpar 297 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π) β π β dom πΉ) |
82 | 78, 81 | syldan 282 |
. . . . . . . . . . . . . . 15
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β dom πΉ) |
83 | 82 | adantlr 477 |
. . . . . . . . . . . . . 14
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β π β dom πΉ) |
84 | 83 | adantlr 477 |
. . . . . . . . . . . . 13
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β π β dom πΉ) |
85 | | funimass3 5633 |
. . . . . . . . . . . . 13
β’ ((Fun
πΉ β§ π β dom πΉ) β ((πΉ β π) β π β π β (β‘πΉ β π))) |
86 | 76, 84, 85 | syl2anc 411 |
. . . . . . . . . . . 12
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β ((πΉ β π) β π β π β (β‘πΉ β π))) |
87 | 75, 86 | anbi12d 473 |
. . . . . . . . . . 11
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β ((π΄ β π β§ (πΉ β π) β π) β ({π΄} β π β§ π β (β‘πΉ β π)))) |
88 | 87 | biimprd 158 |
. . . . . . . . . 10
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β (({π΄} β π β§ π β (β‘πΉ β π)) β (π΄ β π β§ (πΉ β π) β π))) |
89 | 88 | reximdva 2579 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)) β βπ β π½ (π΄ β π β§ (πΉ β π) β π))) |
90 | 69, 73, 89 | 3syld 57 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β βπ β π½ (π΄ β π β§ (πΉ β π) β π))) |
91 | 90 | exp32 365 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β ((πΉβπ΄) β π β (π β πΎ β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
92 | 91 | com24 87 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (π β πΎ β ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
93 | 92 | imp 124 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β (π β πΎ β ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π)))) |
94 | 93 | ralrimiv 2549 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))) |
95 | 11 | 3ad2ant1 1018 |
. . . . . . . 8
β’ ((π½ β Top β§ πΎ β Top β§ π΄ β π) β π½ β (TopOnβπ)) |
96 | 16 | 3ad2ant2 1019 |
. . . . . . . 8
β’ ((π½ β Top β§ πΎ β Top β§ π΄ β π) β πΎ β (TopOnβπ)) |
97 | | simp3 999 |
. . . . . . . 8
β’ ((π½ β Top β§ πΎ β Top β§ π΄ β π) β π΄ β π) |
98 | | iscnp 13702 |
. . . . . . . 8
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
99 | 95, 96, 97, 98 | syl3anc 1238 |
. . . . . . 7
β’ ((π½ β Top β§ πΎ β Top β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
100 | 99 | 3expa 1203 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
101 | 100 | 3adantl3 1155 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
102 | 101 | adantr 276 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
103 | 60, 94, 102 | mpbir2and 944 |
. . 3
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β πΉ β ((π½ CnP πΎ)βπ΄)) |
104 | 103 | ex 115 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β πΉ β ((π½ CnP πΎ)βπ΄))) |
105 | 59, 104 | impbid 129 |
1
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}))) |