Step | Hyp | Ref
| Expression |
1 | | cnvimass 6078 |
. . . . . . . 8
β’ (β‘πΉ β π¦) β dom πΉ |
2 | | fdm 6724 |
. . . . . . . 8
β’ (πΉ:πβΆπ β dom πΉ = π) |
3 | 1, 2 | sseqtrid 4034 |
. . . . . . 7
β’ (πΉ:πβΆπ β (β‘πΉ β π¦) β π) |
4 | 3 | 3ad2ant3 1136 |
. . . . . 6
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (β‘πΉ β π¦) β π) |
5 | 4 | ad2antrr 725 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β (β‘πΉ β π¦) β π) |
6 | | neii2 22604 |
. . . . . . . 8
β’ ((πΎ β Top β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β βπ β πΎ ({(πΉβπ΄)} β π β§ π β π¦)) |
7 | 6 | 3ad2antl2 1187 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β βπ β πΎ ({(πΉβπ΄)} β π β§ π β π¦)) |
8 | 7 | ad2ant2rl 748 |
. . . . . 6
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β βπ β πΎ ({(πΉβπ΄)} β π β§ π β π¦)) |
9 | | simpll 766 |
. . . . . . . . . 10
β’ (((πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β πΉ β ((π½ CnP πΎ)βπ΄)) |
10 | | simprl 770 |
. . . . . . . . . 10
β’ (((πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β π β πΎ) |
11 | | fvex 6902 |
. . . . . . . . . . . . . 14
β’ (πΉβπ΄) β V |
12 | 11 | snss 4789 |
. . . . . . . . . . . . 13
β’ ((πΉβπ΄) β π β {(πΉβπ΄)} β π) |
13 | 12 | biimpri 227 |
. . . . . . . . . . . 12
β’ ({(πΉβπ΄)} β π β (πΉβπ΄) β π) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
β’ (({(πΉβπ΄)} β π β§ π β π¦) β (πΉβπ΄) β π) |
15 | 14 | ad2antll 728 |
. . . . . . . . . 10
β’ (((πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (πΉβπ΄) β π) |
16 | 9, 10, 15 | 3jca 1129 |
. . . . . . . . 9
β’ (((πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)})) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (πΉ β ((π½ CnP πΎ)βπ΄) β§ π β πΎ β§ (πΉβπ΄) β π)) |
17 | 16 | adantll 713 |
. . . . . . . 8
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (πΉ β ((π½ CnP πΎ)βπ΄) β§ π β πΎ β§ (πΉβπ΄) β π)) |
18 | | cnpimaex 22752 |
. . . . . . . 8
β’ ((πΉ β ((π½ CnP πΎ)βπ΄) β§ π β πΎ β§ (πΉβπ΄) β π) β βπ β π½ (π΄ β π β§ (πΉ β π) β π)) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β βπ β π½ (π΄ β π β§ (πΉ β π) β π)) |
20 | | sstr2 3989 |
. . . . . . . . . . . . 13
β’ ((πΉ β π) β π β (π β π¦ β (πΉ β π) β π¦)) |
21 | 20 | com12 32 |
. . . . . . . . . . . 12
β’ (π β π¦ β ((πΉ β π) β π β (πΉ β π) β π¦)) |
22 | 21 | ad2antll 728 |
. . . . . . . . . . 11
β’ ((π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦)) β ((πΉ β π) β π β (πΉ β π) β π¦)) |
23 | 22 | ad2antlr 726 |
. . . . . . . . . 10
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((πΉ β π) β π β (πΉ β π) β π¦)) |
24 | | ffun 6718 |
. . . . . . . . . . . . . 14
β’ (πΉ:πβΆπ β Fun πΉ) |
25 | 24 | 3ad2ant3 1136 |
. . . . . . . . . . . . 13
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β Fun πΉ) |
26 | 25 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β Fun πΉ) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . 11
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β Fun πΉ) |
28 | | cnpnei.1 |
. . . . . . . . . . . . . . . . 17
β’ π = βͺ
π½ |
29 | 28 | eltopss 22401 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π β π½) β π β π) |
30 | 29 | adantlr 714 |
. . . . . . . . . . . . . . 15
β’ (((π½ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β π) |
31 | 2 | sseq2d 4014 |
. . . . . . . . . . . . . . . 16
β’ (πΉ:πβΆπ β (π β dom πΉ β π β π)) |
32 | 31 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π½ β Top β§ πΉ:πβΆπ) β§ π β π½) β (π β dom πΉ β π β π)) |
33 | 30, 32 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ (((π½ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β dom πΉ) |
34 | 33 | 3adantl2 1168 |
. . . . . . . . . . . . 13
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β dom πΉ) |
35 | 34 | adantlr 714 |
. . . . . . . . . . . 12
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ π β π½) β π β dom πΉ) |
36 | 35 | ad4ant14 751 |
. . . . . . . . . . 11
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β π β dom πΉ) |
37 | | funimass3 7053 |
. . . . . . . . . . 11
β’ ((Fun
πΉ β§ π β dom πΉ) β ((πΉ β π) β π¦ β π β (β‘πΉ β π¦))) |
38 | 27, 36, 37 | syl2anc 585 |
. . . . . . . . . 10
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((πΉ β π) β π¦ β π β (β‘πΉ β π¦))) |
39 | 23, 38 | sylibd 238 |
. . . . . . . . 9
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((πΉ β π) β π β π β (β‘πΉ β π¦))) |
40 | 39 | anim2d 613 |
. . . . . . . 8
β’
((((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β§ π β π½) β ((π΄ β π β§ (πΉ β π) β π) β (π΄ β π β§ π β (β‘πΉ β π¦)))) |
41 | 40 | reximdva 3169 |
. . . . . . 7
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β (βπ β π½ (π΄ β π β§ (πΉ β π) β π) β βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦)))) |
42 | 19, 41 | mpd 15 |
. . . . . 6
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β§ (π β πΎ β§ ({(πΉβπ΄)} β π β§ π β π¦))) β βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))) |
43 | 8, 42 | rexlimddv 3162 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))) |
44 | 28 | isneip 22601 |
. . . . . . 7
β’ ((π½ β Top β§ π΄ β π) β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β ((β‘πΉ β π¦) β π β§ βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))))) |
45 | 44 | 3ad2antl1 1186 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β ((β‘πΉ β π¦) β π β§ βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))))) |
46 | 45 | adantr 482 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β ((β‘πΉ β π¦) β π β§ βπ β π½ (π΄ β π β§ π β (β‘πΉ β π¦))))) |
47 | 5, 43, 46 | mpbir2and 712 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ (πΉ β ((π½ CnP πΎ)βπ΄) β§ π¦ β ((neiβπΎ)β{(πΉβπ΄)}))) β (β‘πΉ β π¦) β ((neiβπ½)β{π΄})) |
48 | 47 | exp32 422 |
. . 3
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π¦ β ((neiβπΎ)β{(πΉβπ΄)}) β (β‘πΉ β π¦) β ((neiβπ½)β{π΄})))) |
49 | 48 | ralrimdv 3153 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}))) |
50 | | simpll3 1215 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β πΉ:πβΆπ) |
51 | | opnneip 22615 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Top β§ π β πΎ β§ (πΉβπ΄) β π) β π β ((neiβπΎ)β{(πΉβπ΄)})) |
52 | | imaeq2 6054 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π β (β‘πΉ β π¦) = (β‘πΉ β π)) |
53 | 52 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β ((β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
54 | 53 | rspcv 3609 |
. . . . . . . . . . . . . 14
β’ (π β ((neiβπΎ)β{(πΉβπ΄)}) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
55 | 51, 54 | syl 17 |
. . . . . . . . . . . . 13
β’ ((πΎ β Top β§ π β πΎ β§ (πΉβπ΄) β π) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
56 | 55 | 3com23 1127 |
. . . . . . . . . . . 12
β’ ((πΎ β Top β§ (πΉβπ΄) β π β§ π β πΎ) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
57 | 56 | 3expb 1121 |
. . . . . . . . . . 11
β’ ((πΎ β Top β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
58 | 57 | 3ad2antl2 1187 |
. . . . . . . . . 10
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
59 | 58 | adantlr 714 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (β‘πΉ β π) β ((neiβπ½)β{π΄}))) |
60 | | neii2 22604 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ (β‘πΉ β π) β ((neiβπ½)β{π΄})) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π))) |
61 | 60 | ex 414 |
. . . . . . . . . . 11
β’ (π½ β Top β ((β‘πΉ β π) β ((neiβπ½)β{π΄}) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)))) |
62 | 61 | 3ad2ant1 1134 |
. . . . . . . . . 10
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β ((β‘πΉ β π) β ((neiβπ½)β{π΄}) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)))) |
63 | 62 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β ((β‘πΉ β π) β ((neiβπ½)β{π΄}) β βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)))) |
64 | | snssg 4787 |
. . . . . . . . . . . . 13
β’ (π΄ β π β (π΄ β π β {π΄} β π)) |
65 | 64 | ad3antlr 730 |
. . . . . . . . . . . 12
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β (π΄ β π β {π΄} β π)) |
66 | 25 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β Fun πΉ) |
67 | 28 | eltopss 22401 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ π β π½) β π β π) |
68 | 67 | 3ad2antl1 1186 |
. . . . . . . . . . . . . . 15
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β π) |
69 | 2 | sseq2d 4014 |
. . . . . . . . . . . . . . . . 17
β’ (πΉ:πβΆπ β (π β dom πΉ β π β π)) |
70 | 69 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β (π β dom πΉ β π β π)) |
71 | 70 | biimpar 479 |
. . . . . . . . . . . . . . 15
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π) β π β dom πΉ) |
72 | 68, 71 | syldan 592 |
. . . . . . . . . . . . . 14
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π β π½) β π β dom πΉ) |
73 | 72 | ad4ant14 751 |
. . . . . . . . . . . . 13
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β π β dom πΉ) |
74 | | funimass3 7053 |
. . . . . . . . . . . . 13
β’ ((Fun
πΉ β§ π β dom πΉ) β ((πΉ β π) β π β π β (β‘πΉ β π))) |
75 | 66, 73, 74 | syl2anc 585 |
. . . . . . . . . . . 12
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β ((πΉ β π) β π β π β (β‘πΉ β π))) |
76 | 65, 75 | anbi12d 632 |
. . . . . . . . . . 11
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β ((π΄ β π β§ (πΉ β π) β π) β ({π΄} β π β§ π β (β‘πΉ β π)))) |
77 | 76 | biimprd 247 |
. . . . . . . . . 10
β’
(((((π½ β Top
β§ πΎ β Top β§
πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β§ π β π½) β (({π΄} β π β§ π β (β‘πΉ β π)) β (π΄ β π β§ (πΉ β π) β π))) |
78 | 77 | reximdva 3169 |
. . . . . . . . 9
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ β π½ ({π΄} β π β§ π β (β‘πΉ β π)) β βπ β π½ (π΄ β π β§ (πΉ β π) β π))) |
79 | 59, 63, 78 | 3syld 60 |
. . . . . . . 8
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ ((πΉβπ΄) β π β§ π β πΎ)) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β βπ β π½ (π΄ β π β§ (πΉ β π) β π))) |
80 | 79 | exp32 422 |
. . . . . . 7
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β ((πΉβπ΄) β π β (π β πΎ β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
81 | 80 | com24 95 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β (π β πΎ β ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
82 | 81 | imp 408 |
. . . . 5
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β (π β πΎ β ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π)))) |
83 | 82 | ralrimiv 3146 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))) |
84 | | cnpnei.2 |
. . . . . . . . 9
β’ π = βͺ
πΎ |
85 | 28, 84 | iscnp2 22735 |
. . . . . . . 8
β’ (πΉ β ((π½ CnP πΎ)βπ΄) β ((π½ β Top β§ πΎ β Top β§ π΄ β π) β§ (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
86 | 85 | baib 537 |
. . . . . . 7
β’ ((π½ β Top β§ πΎ β Top β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
87 | 86 | 3expa 1119 |
. . . . . 6
β’ (((π½ β Top β§ πΎ β Top) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
88 | 87 | 3adantl3 1169 |
. . . . 5
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
89 | 88 | adantr 482 |
. . . 4
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β πΎ ((πΉβπ΄) β π β βπ β π½ (π΄ β π β§ (πΉ β π) β π))))) |
90 | 50, 83, 89 | mpbir2and 712 |
. . 3
β’ ((((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β§ βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄})) β πΉ β ((π½ CnP πΎ)βπ΄)) |
91 | 90 | ex 414 |
. 2
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}) β πΉ β ((π½ CnP πΎ)βπ΄))) |
92 | 49, 91 | impbid 211 |
1
β’ (((π½ β Top β§ πΎ β Top β§ πΉ:πβΆπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β βπ¦ β ((neiβπΎ)β{(πΉβπ΄)})(β‘πΉ β π¦) β ((neiβπ½)β{π΄}))) |