Step | Hyp | Ref
| Expression |
1 | | tgcn.1 |
. . . 4
β’ (π β π½ β (TopOnβπ)) |
2 | | tgcn.4 |
. . . 4
β’ (π β πΎ β (TopOnβπ)) |
3 | | tgcnp.5 |
. . . 4
β’ (π β π β π) |
4 | | iscnp 22741 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
5 | 1, 2, 3, 4 | syl3anc 1372 |
. . 3
β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
6 | | tgcn.3 |
. . . . . . . . 9
β’ (π β πΎ = (topGenβπ΅)) |
7 | | topontop 22415 |
. . . . . . . . . 10
β’ (πΎ β (TopOnβπ) β πΎ β Top) |
8 | 2, 7 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ β Top) |
9 | 6, 8 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β (topGenβπ΅) β Top) |
10 | | tgclb 22473 |
. . . . . . . 8
β’ (π΅ β TopBases β
(topGenβπ΅) β
Top) |
11 | 9, 10 | sylibr 233 |
. . . . . . 7
β’ (π β π΅ β TopBases) |
12 | | bastg 22469 |
. . . . . . 7
β’ (π΅ β TopBases β π΅ β (topGenβπ΅)) |
13 | 11, 12 | syl 17 |
. . . . . 6
β’ (π β π΅ β (topGenβπ΅)) |
14 | 13, 6 | sseqtrrd 4024 |
. . . . 5
β’ (π β π΅ β πΎ) |
15 | | ssralv 4051 |
. . . . 5
β’ (π΅ β πΎ β (βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)))) |
16 | 14, 15 | syl 17 |
. . . 4
β’ (π β (βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)))) |
17 | 16 | anim2d 613 |
. . 3
β’ (π β ((πΉ:πβΆπ β§ βπ¦ β πΎ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))) β (πΉ:πβΆπ β§ βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
18 | 5, 17 | sylbid 239 |
. 2
β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |
19 | 6 | eleq2d 2820 |
. . . . . . 7
β’ (π β (π§ β πΎ β π§ β (topGenβπ΅))) |
20 | 19 | biimpa 478 |
. . . . . 6
β’ ((π β§ π§ β πΎ) β π§ β (topGenβπ΅)) |
21 | | tg2 22468 |
. . . . . . . . 9
β’ ((π§ β (topGenβπ΅) β§ (πΉβπ) β π§) β βπ¦ β π΅ ((πΉβπ) β π¦ β§ π¦ β π§)) |
22 | | r19.29 3115 |
. . . . . . . . . . 11
β’
((βπ¦ β
π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β§ βπ¦ β π΅ ((πΉβπ) β π¦ β§ π¦ β π§)) β βπ¦ β π΅ (((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β§ ((πΉβπ) β π¦ β§ π¦ β π§))) |
23 | | sstr 3991 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΉ β π₯) β π¦ β§ π¦ β π§) β (πΉ β π₯) β π§) |
24 | 23 | expcom 415 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β π§ β ((πΉ β π₯) β π¦ β (πΉ β π₯) β π§)) |
25 | 24 | anim2d 613 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β π§ β ((π β π₯ β§ (πΉ β π₯) β π¦) β (π β π₯ β§ (πΉ β π₯) β π§))) |
26 | 25 | reximdv 3171 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π§ β (βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))) |
27 | 26 | com12 32 |
. . . . . . . . . . . . . 14
β’
(βπ₯ β
π½ (π β π₯ β§ (πΉ β π₯) β π¦) β (π¦ β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))) |
28 | 27 | imim2i 16 |
. . . . . . . . . . . . 13
β’ (((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β ((πΉβπ) β π¦ β (π¦ β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)))) |
29 | 28 | imp32 420 |
. . . . . . . . . . . 12
β’ ((((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β§ ((πΉβπ) β π¦ β§ π¦ β π§)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)) |
30 | 29 | rexlimivw 3152 |
. . . . . . . . . . 11
β’
(βπ¦ β
π΅ (((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β§ ((πΉβπ) β π¦ β§ π¦ β π§)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)) |
31 | 22, 30 | syl 17 |
. . . . . . . . . 10
β’
((βπ¦ β
π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β§ βπ¦ β π΅ ((πΉβπ) β π¦ β§ π¦ β π§)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)) |
32 | 31 | expcom 415 |
. . . . . . . . 9
β’
(βπ¦ β
π΅ ((πΉβπ) β π¦ β§ π¦ β π§) β (βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))) |
33 | 21, 32 | syl 17 |
. . . . . . . 8
β’ ((π§ β (topGenβπ΅) β§ (πΉβπ) β π§) β (βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))) |
34 | 33 | ex 414 |
. . . . . . 7
β’ (π§ β (topGenβπ΅) β ((πΉβπ) β π§ β (βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)))) |
35 | 34 | com23 86 |
. . . . . 6
β’ (π§ β (topGenβπ΅) β (βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β ((πΉβπ) β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)))) |
36 | 20, 35 | syl 17 |
. . . . 5
β’ ((π β§ π§ β πΎ) β (βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β ((πΉβπ) β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)))) |
37 | 36 | ralrimdva 3155 |
. . . 4
β’ (π β (βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦)) β βπ§ β πΎ ((πΉβπ) β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§)))) |
38 | 37 | anim2d 613 |
. . 3
β’ (π β ((πΉ:πβΆπ β§ βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))) β (πΉ:πβΆπ β§ βπ§ β πΎ ((πΉβπ) β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))))) |
39 | | iscnp 22741 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π β π) β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ§ β πΎ ((πΉβπ) β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))))) |
40 | 1, 2, 3, 39 | syl3anc 1372 |
. . 3
β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ§ β πΎ ((πΉβπ) β π§ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π§))))) |
41 | 38, 40 | sylibrd 259 |
. 2
β’ (π β ((πΉ:πβΆπ β§ βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))) β πΉ β ((π½ CnP πΎ)βπ))) |
42 | 18, 41 | impbid 211 |
1
β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ¦ β π΅ ((πΉβπ) β π¦ β βπ₯ β π½ (π β π₯ β§ (πΉ β π₯) β π¦))))) |