Step | Hyp | Ref
| Expression |
1 | | eldif 3921 |
. . . . . . . . . 10
β’ (π₯ β (π β βͺ (π΅ β πΉ)) β (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) |
2 | | alexsub.3 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π½ = (topGenβ(fiβπ΅))) |
3 | 2 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π¦ β π½ β π¦ β (topGenβ(fiβπ΅)))) |
4 | 3 | anbi1d 631 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((π¦ β π½ β§ π₯ β π¦) β (π¦ β (topGenβ(fiβπ΅)) β§ π₯ β π¦))) |
5 | 4 | biimpa 478 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π¦ β π½ β§ π₯ β π¦)) β (π¦ β (topGenβ(fiβπ΅)) β§ π₯ β π¦)) |
6 | 5 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β (π¦ β (topGenβ(fiβπ΅)) β§ π₯ β π¦)) |
7 | | tg2 22331 |
. . . . . . . . . . . . . . . 16
β’ ((π¦ β
(topGenβ(fiβπ΅))
β§ π₯ β π¦) β βπ§ β (fiβπ΅)(π₯ β π§ β§ π§ β π¦)) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β βπ§ β (fiβπ΅)(π₯ β π§ β§ π§ β π¦)) |
9 | | alexsub.5 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΉ β (UFilβπ)) |
10 | | ufilfil 23271 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ β (UFilβπ) β πΉ β (Filβπ)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ β (Filβπ)) |
12 | 11 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β§ (π§ β (fiβπ΅) β§ (π₯ β π§ β§ π§ β π¦))) β πΉ β (Filβπ)) |
13 | | alexsub.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π = βͺ π΅) |
14 | 9 | elfvexd 6882 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π β V) |
15 | 13, 14 | eqeltrrd 2835 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βͺ π΅
β V) |
16 | | uniexb 7699 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π΅ β V β βͺ π΅
β V) |
17 | 15, 16 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π΅ β V) |
18 | | elfi2 9355 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π΅ β V β (π§ β (fiβπ΅) β βπ¦ β ((π« π΅ β© Fin) β
{β
})π§ = β© π¦)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π§ β (fiβπ΅) β βπ¦ β ((π« π΅ β© Fin) β {β
})π§ = β©
π¦)) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β (π§ β (fiβπ΅) β βπ¦ β ((π« π΅ β© Fin) β {β
})π§ = β©
π¦)) |
21 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β πΉ β
(Filβπ)) |
22 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β Β¬ π₯ β βͺ (π΅
β πΉ)) |
23 | | intss1 4925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ β π¦ β β© π¦ β π§) |
24 | 23 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π¦ β ((π« π΅ β© Fin) β {β
})
β§ π₯ β β© π¦)
β§ π§ β π¦) β β© π¦
β π§) |
25 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π¦ β ((π« π΅ β© Fin) β {β
})
β§ π₯ β β© π¦)
β§ π§ β π¦) β π₯ β β© π¦) |
26 | 24, 25 | sseldd 3946 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π¦ β ((π« π΅ β© Fin) β {β
})
β§ π₯ β β© π¦)
β§ π§ β π¦) β π₯ β π§) |
27 | 26 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β§ Β¬ π§ β πΉ) β π₯ β π§) |
28 | | eldifsn 4748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π¦ β ((π« π΅ β© Fin) β {β
})
β (π¦ β (π«
π΅ β© Fin) β§ π¦ β β
)) |
29 | 28 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π¦ β ((π« π΅ β© Fin) β {β
})
β π¦ β (π«
π΅ β©
Fin)) |
30 | 29 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β π¦ β (π«
π΅ β©
Fin)) |
31 | | elfpw 9301 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π¦ β (π« π΅ β© Fin) β (π¦ β π΅ β§ π¦ β Fin)) |
32 | 31 | simplbi 499 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π¦ β (π« π΅ β© Fin) β π¦ β π΅) |
33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β π¦ β π΅) |
34 | 33 | sselda 3945 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β§ π§ β π¦) β π§ β π΅) |
35 | 34 | anasss 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β π§ β π΅) |
36 | 35 | anim1i 616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β§ Β¬ π§ β πΉ) β (π§ β π΅ β§ Β¬ π§ β πΉ)) |
37 | | eldif 3921 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ β (π΅ β πΉ) β (π§ β π΅ β§ Β¬ π§ β πΉ)) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β§ Β¬ π§ β πΉ) β π§ β (π΅ β πΉ)) |
39 | | elunii 4871 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π₯ β π§ β§ π§ β (π΅ β πΉ)) β π₯ β βͺ (π΅ β πΉ)) |
40 | 27, 38, 39 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β§ Β¬ π§ β πΉ) β π₯ β βͺ (π΅ β πΉ)) |
41 | 40 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β (Β¬ π§ β πΉ β π₯ β βͺ (π΅ β πΉ))) |
42 | 22, 41 | mt3d 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ ((π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦)
β§ π§ β π¦)) β π§ β πΉ) |
43 | 42 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β (π§ β π¦ β π§ β πΉ)) |
44 | 43 | ssrdv 3951 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β π¦ β πΉ) |
45 | | eldifsni 4751 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β ((π« π΅ β© Fin) β {β
})
β π¦ β
β
) |
46 | 45 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β π¦ β
β
) |
47 | | elinel2 4157 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π¦ β (π« π΅ β© Fin) β π¦ β Fin) |
48 | 30, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β π¦ β
Fin) |
49 | | elfir 9356 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉ β (Filβπ) β§ (π¦ β πΉ β§ π¦ β β
β§ π¦ β Fin)) β β© π¦
β (fiβπΉ)) |
50 | 21, 44, 46, 48, 49 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β β© π¦ β (fiβπΉ)) |
51 | | filfi 23226 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (πΉ β (Filβπ) β (fiβπΉ) = πΉ) |
52 | 21, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β (fiβπΉ) = πΉ) |
53 | 50, 52 | eleqtrd 2836 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β ((π« π΅ β© Fin) β {β
}) β§ π₯ β β© π¦))
β β© π¦ β πΉ) |
54 | 53 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ π¦ β ((π« π΅ β© Fin) β {β
})) β
(π₯ β β© π¦
β β© π¦ β πΉ)) |
55 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = β©
π¦ β (π₯ β π§ β π₯ β β© π¦)) |
56 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = β©
π¦ β (π§ β πΉ β β© π¦ β πΉ)) |
57 | 55, 56 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π§ = β©
π¦ β ((π₯ β π§ β π§ β πΉ) β (π₯ β β© π¦ β β© π¦
β πΉ))) |
58 | 54, 57 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ π¦ β ((π« π΅ β© Fin) β {β
})) β
(π§ = β© π¦
β (π₯ β π§ β π§ β πΉ))) |
59 | 58 | rexlimdva 3149 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β (βπ¦ β ((π« π΅ β© Fin) β {β
})π§ = β©
π¦ β (π₯ β π§ β π§ β πΉ))) |
60 | 20, 59 | sylbid 239 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β (π§ β (fiβπ΅) β (π₯ β π§ β π§ β πΉ))) |
61 | 60 | imp32 420 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π§ β (fiβπ΅) β§ π₯ β π§)) β π§ β πΉ) |
62 | 61 | adantrrr 724 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π§ β (fiβπ΅) β§ (π₯ β π§ β§ π§ β π¦))) β π§ β πΉ) |
63 | 62 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β§ (π§ β (fiβπ΅) β§ (π₯ β π§ β§ π§ β π¦))) β π§ β πΉ) |
64 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . . 19
β’ (π¦ β π½ β π¦ β βͺ π½) |
65 | 64 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β βͺ π½) |
66 | | fibas 22343 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(fiβπ΅) β
TopBases |
67 | | tgtopon 22337 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((fiβπ΅) β
TopBases β (topGenβ(fiβπ΅)) β (TopOnββͺ (fiβπ΅))) |
68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(topGenβ(fiβπ΅)) β (TopOnββͺ (fiβπ΅)) |
69 | 2, 68 | eqeltrdi 2842 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π½ β (TopOnββͺ (fiβπ΅))) |
70 | | fiuni 9369 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π΅ β V β βͺ π΅ =
βͺ (fiβπ΅)) |
71 | 17, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β βͺ π΅ =
βͺ (fiβπ΅)) |
72 | 13, 71 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β π = βͺ
(fiβπ΅)) |
73 | 72 | fveq2d 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (TopOnβπ) = (TopOnββͺ (fiβπ΅))) |
74 | 69, 73 | eleqtrrd 2837 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π½ β (TopOnβπ)) |
75 | | toponuni 22279 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π½ β (TopOnβπ) β π = βͺ π½) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π = βͺ π½) |
77 | 76 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β π = βͺ π½) |
78 | 65, 77 | sseqtrrd 3986 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β π) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β§ (π§ β (fiβπ΅) β§ (π₯ β π§ β§ π§ β π¦))) β π¦ β π) |
80 | | simprrr 781 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β§ (π§ β (fiβπ΅) β§ (π₯ β π§ β§ π§ β π¦))) β π§ β π¦) |
81 | | filss 23220 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β (Filβπ) β§ (π§ β πΉ β§ π¦ β π β§ π§ β π¦)) β π¦ β πΉ) |
82 | 12, 63, 79, 80, 81 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β§ (π§ β (fiβπ΅) β§ (π₯ β π§ β§ π§ β π¦))) β π¦ β πΉ) |
83 | 8, 82 | rexlimddv 3155 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ (π¦ β π½ β§ π₯ β π¦)) β π¦ β πΉ) |
84 | 83 | expr 458 |
. . . . . . . . . . . . 13
β’ (((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β§ π¦ β π½) β (π₯ β π¦ β π¦ β πΉ)) |
85 | 84 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ))) β βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)) |
86 | 85 | expr 458 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β (Β¬ π₯ β βͺ (π΅ β πΉ) β βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ))) |
87 | 86 | imdistanda 573 |
. . . . . . . . . 10
β’ (π β ((π₯ β π β§ Β¬ π₯ β βͺ (π΅ β πΉ)) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
88 | 1, 87 | biimtrid 241 |
. . . . . . . . 9
β’ (π β (π₯ β (π β βͺ (π΅ β πΉ)) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
89 | | flimopn 23342 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π₯ β (π½ fLim πΉ) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
90 | 74, 11, 89 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π₯ β (π½ fLim πΉ) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΉ)))) |
91 | 88, 90 | sylibrd 259 |
. . . . . . . 8
β’ (π β (π₯ β (π β βͺ (π΅ β πΉ)) β π₯ β (π½ fLim πΉ))) |
92 | 91 | ssrdv 3951 |
. . . . . . 7
β’ (π β (π β βͺ (π΅ β πΉ)) β (π½ fLim πΉ)) |
93 | | alexsub.6 |
. . . . . . 7
β’ (π β (π½ fLim πΉ) = β
) |
94 | | sseq0 4360 |
. . . . . . 7
β’ (((π β βͺ (π΅
β πΉ)) β (π½ fLim πΉ) β§ (π½ fLim πΉ) = β
) β (π β βͺ (π΅ β πΉ)) = β
) |
95 | 92, 93, 94 | syl2anc 585 |
. . . . . 6
β’ (π β (π β βͺ (π΅ β πΉ)) = β
) |
96 | | ssdif0 4324 |
. . . . . 6
β’ (π β βͺ (π΅
β πΉ) β (π β βͺ (π΅
β πΉ)) =
β
) |
97 | 95, 96 | sylibr 233 |
. . . . 5
β’ (π β π β βͺ (π΅ β πΉ)) |
98 | | difss 4092 |
. . . . . . 7
β’ (π΅ β πΉ) β π΅ |
99 | 98 | unissi 4875 |
. . . . . 6
β’ βͺ (π΅
β πΉ) β βͺ π΅ |
100 | 99, 13 | sseqtrrid 3998 |
. . . . 5
β’ (π β βͺ (π΅
β πΉ) β π) |
101 | 97, 100 | eqssd 3962 |
. . . 4
β’ (π β π = βͺ (π΅ β πΉ)) |
102 | 101, 98 | jctil 521 |
. . 3
β’ (π β ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ))) |
103 | 17 | difexd 5287 |
. . . . 5
β’ (π β (π΅ β πΉ) β V) |
104 | 103 | adantr 482 |
. . . 4
β’ ((π β§ ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ))) β (π΅ β πΉ) β V) |
105 | | sseq1 3970 |
. . . . . . . 8
β’ (π₯ = (π΅ β πΉ) β (π₯ β π΅ β (π΅ β πΉ) β π΅)) |
106 | | unieq 4877 |
. . . . . . . . 9
β’ (π₯ = (π΅ β πΉ) β βͺ π₯ = βͺ
(π΅ β πΉ)) |
107 | 106 | eqeq2d 2744 |
. . . . . . . 8
β’ (π₯ = (π΅ β πΉ) β (π = βͺ π₯ β π = βͺ (π΅ β πΉ))) |
108 | 105, 107 | anbi12d 632 |
. . . . . . 7
β’ (π₯ = (π΅ β πΉ) β ((π₯ β π΅ β§ π = βͺ π₯) β ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ)))) |
109 | 108 | anbi2d 630 |
. . . . . 6
β’ (π₯ = (π΅ β πΉ) β ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β (π β§ ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ))))) |
110 | | pweq 4575 |
. . . . . . . 8
β’ (π₯ = (π΅ β πΉ) β π« π₯ = π« (π΅ β πΉ)) |
111 | 110 | ineq1d 4172 |
. . . . . . 7
β’ (π₯ = (π΅ β πΉ) β (π« π₯ β© Fin) = (π« (π΅ β πΉ) β© Fin)) |
112 | 111 | rexeqdv 3313 |
. . . . . 6
β’ (π₯ = (π΅ β πΉ) β (βπ¦ β (π« π₯ β© Fin)π = βͺ π¦ β βπ¦ β (π« (π΅ β πΉ) β© Fin)π = βͺ π¦)) |
113 | 109, 112 | imbi12d 345 |
. . . . 5
β’ (π₯ = (π΅ β πΉ) β (((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β ((π β§ ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ))) β βπ¦ β (π« (π΅ β πΉ) β© Fin)π = βͺ π¦))) |
114 | | alexsub.4 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) |
115 | 113, 114 | vtoclg 3524 |
. . . 4
β’ ((π΅ β πΉ) β V β ((π β§ ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ))) β βπ¦ β (π« (π΅ β πΉ) β© Fin)π = βͺ π¦)) |
116 | 104, 115 | mpcom 38 |
. . 3
β’ ((π β§ ((π΅ β πΉ) β π΅ β§ π = βͺ (π΅ β πΉ))) β βπ¦ β (π« (π΅ β πΉ) β© Fin)π = βͺ π¦) |
117 | 102, 116 | mpdan 686 |
. 2
β’ (π β βπ¦ β (π« (π΅ β πΉ) β© Fin)π = βͺ π¦) |
118 | | unieq 4877 |
. . . . . . 7
β’ (π¦ = β
β βͺ π¦ =
βͺ β
) |
119 | | uni0 4897 |
. . . . . . 7
β’ βͺ β
= β
|
120 | 118, 119 | eqtrdi 2789 |
. . . . . 6
β’ (π¦ = β
β βͺ π¦ =
β
) |
121 | 120 | neeq2d 3001 |
. . . . 5
β’ (π¦ = β
β (π β βͺ π¦
β π β
β
)) |
122 | | difssd 4093 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β (π β π§) β π) |
123 | 122 | ralrimivw 3144 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β βπ§ β π¦ (π β π§) β π) |
124 | | riinn0 5044 |
. . . . . . . . . 10
β’
((βπ§ β
π¦ (π β π§) β π β§ π¦ β β
) β (π β© β©
π§ β π¦ (π β π§)) = β©
π§ β π¦ (π β π§)) |
125 | 123, 124 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β (π β© β©
π§ β π¦ (π β π§)) = β©
π§ β π¦ (π β π§)) |
126 | 14 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π β V) |
127 | 126 | difexd 5287 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β (π β π§) β V) |
128 | 127 | ralrimivw 3144 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β βπ§ β π¦ (π β π§) β V) |
129 | | dfiin2g 4993 |
. . . . . . . . . . 11
β’
(βπ§ β
π¦ (π β π§) β V β β© π§ β π¦ (π β π§) = β© {π₯ β£ βπ§ β π¦ π₯ = (π β π§)}) |
130 | 128, 129 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β β© π§ β π¦ (π β π§) = β© {π₯ β£ βπ§ β π¦ π₯ = (π β π§)}) |
131 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π§ β π¦ β¦ (π β π§)) = (π§ β π¦ β¦ (π β π§)) |
132 | 131 | rnmpt 5911 |
. . . . . . . . . . 11
β’ ran
(π§ β π¦ β¦ (π β π§)) = {π₯ β£ βπ§ β π¦ π₯ = (π β π§)} |
133 | 132 | inteqi 4912 |
. . . . . . . . . 10
β’ β© ran (π§ β π¦ β¦ (π β π§)) = β© {π₯ β£ βπ§ β π¦ π₯ = (π β π§)} |
134 | 130, 133 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β β© π§ β π¦ (π β π§) = β© ran (π§ β π¦ β¦ (π β π§))) |
135 | 125, 134 | eqtrd 2773 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β (π β© β©
π§ β π¦ (π β π§)) = β© ran (π§ β π¦ β¦ (π β π§))) |
136 | 11 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β πΉ β (Filβπ)) |
137 | | elfpw 9301 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β (π« (π΅ β πΉ) β© Fin) β (π¦ β (π΅ β πΉ) β§ π¦ β Fin)) |
138 | 137 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π¦ β (π« (π΅ β πΉ) β© Fin) β π¦ β (π΅ β πΉ)) |
139 | 138 | ad2antlr 726 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π¦ β (π΅ β πΉ)) |
140 | 139 | sselda 3945 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β π§ β (π΅ β πΉ)) |
141 | 140 | eldifbd 3924 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β Β¬ π§ β πΉ) |
142 | 9 | ad3antrrr 729 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β πΉ β (UFilβπ)) |
143 | 139 | difss2d 4095 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π¦ β π΅) |
144 | 143 | sselda 3945 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β π§ β π΅) |
145 | | elssuni 4899 |
. . . . . . . . . . . . . . 15
β’ (π§ β π΅ β π§ β βͺ π΅) |
146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β π§ β βͺ π΅) |
147 | 13 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β π = βͺ π΅) |
148 | 146, 147 | sseqtrrd 3986 |
. . . . . . . . . . . . 13
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β π§ β π) |
149 | | ufilb 23273 |
. . . . . . . . . . . . 13
β’ ((πΉ β (UFilβπ) β§ π§ β π) β (Β¬ π§ β πΉ β (π β π§) β πΉ)) |
150 | 142, 148,
149 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β (Β¬ π§ β πΉ β (π β π§) β πΉ)) |
151 | 141, 150 | mpbid 231 |
. . . . . . . . . . 11
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β (π β π§) β πΉ) |
152 | 151 | fmpttd 7064 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β (π§ β π¦ β¦ (π β π§)):π¦βΆπΉ) |
153 | 152 | frnd 6677 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β ran (π§ β π¦ β¦ (π β π§)) β πΉ) |
154 | 131, 151 | dmmptd 6647 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β dom (π§ β π¦ β¦ (π β π§)) = π¦) |
155 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π¦ β β
) |
156 | 154, 155 | eqnetrd 3008 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β dom (π§ β π¦ β¦ (π β π§)) β β
) |
157 | | dm0rn0 5881 |
. . . . . . . . . . 11
β’ (dom
(π§ β π¦ β¦ (π β π§)) = β
β ran (π§ β π¦ β¦ (π β π§)) = β
) |
158 | 157 | necon3bii 2993 |
. . . . . . . . . 10
β’ (dom
(π§ β π¦ β¦ (π β π§)) β β
β ran (π§ β π¦ β¦ (π β π§)) β β
) |
159 | 156, 158 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β ran (π§ β π¦ β¦ (π β π§)) β β
) |
160 | | elinel2 4157 |
. . . . . . . . . . 11
β’ (π¦ β (π« (π΅ β πΉ) β© Fin) β π¦ β Fin) |
161 | 160 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π¦ β Fin) |
162 | | abrexfi 9299 |
. . . . . . . . . . 11
β’ (π¦ β Fin β {π₯ β£ βπ§ β π¦ π₯ = (π β π§)} β Fin) |
163 | 132, 162 | eqeltrid 2838 |
. . . . . . . . . 10
β’ (π¦ β Fin β ran (π§ β π¦ β¦ (π β π§)) β Fin) |
164 | 161, 163 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β ran (π§ β π¦ β¦ (π β π§)) β Fin) |
165 | | filintn0 23228 |
. . . . . . . . 9
β’ ((πΉ β (Filβπ) β§ (ran (π§ β π¦ β¦ (π β π§)) β πΉ β§ ran (π§ β π¦ β¦ (π β π§)) β β
β§ ran (π§ β π¦ β¦ (π β π§)) β Fin)) β β© ran (π§ β π¦ β¦ (π β π§)) β β
) |
166 | 136, 153,
159, 164, 165 | syl13anc 1373 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β β© ran (π§ β π¦ β¦ (π β π§)) β β
) |
167 | 135, 166 | eqnetrd 3008 |
. . . . . . 7
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β (π β© β©
π§ β π¦ (π β π§)) β β
) |
168 | | disj3 4414 |
. . . . . . . 8
β’ ((π β© β© π§ β π¦ (π β π§)) = β
β π = (π β β©
π§ β π¦ (π β π§))) |
169 | 168 | necon3bii 2993 |
. . . . . . 7
β’ ((π β© β© π§ β π¦ (π β π§)) β β
β π β (π β β©
π§ β π¦ (π β π§))) |
170 | 167, 169 | sylib 217 |
. . . . . 6
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π β (π β β©
π§ β π¦ (π β π§))) |
171 | | iundif2 5035 |
. . . . . . 7
β’ βͺ π§ β π¦ (π β (π β π§)) = (π β β©
π§ β π¦ (π β π§)) |
172 | | dfss4 4219 |
. . . . . . . . . 10
β’ (π§ β π β (π β (π β π§)) = π§) |
173 | 148, 172 | sylib 217 |
. . . . . . . . 9
β’ ((((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β§ π§ β π¦) β (π β (π β π§)) = π§) |
174 | 173 | iuneq2dv 4979 |
. . . . . . . 8
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β βͺ π§ β π¦ (π β (π β π§)) = βͺ
π§ β π¦ π§) |
175 | | uniiun 5019 |
. . . . . . . 8
β’ βͺ π¦ =
βͺ π§ β π¦ π§ |
176 | 174, 175 | eqtr4di 2791 |
. . . . . . 7
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β βͺ π§ β π¦ (π β (π β π§)) = βͺ π¦) |
177 | 171, 176 | eqtr3id 2787 |
. . . . . 6
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β (π β β©
π§ β π¦ (π β π§)) = βͺ π¦) |
178 | 170, 177 | neeqtrd 3010 |
. . . . 5
β’ (((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β§ π¦ β β
) β π β βͺ π¦) |
179 | 11 | adantr 482 |
. . . . . 6
β’ ((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β πΉ β (Filβπ)) |
180 | | filtop 23222 |
. . . . . 6
β’ (πΉ β (Filβπ) β π β πΉ) |
181 | | fileln0 23217 |
. . . . . 6
β’ ((πΉ β (Filβπ) β§ π β πΉ) β π β β
) |
182 | 179, 180,
181 | syl2anc2 586 |
. . . . 5
β’ ((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β π β β
) |
183 | 121, 178,
182 | pm2.61ne 3027 |
. . . 4
β’ ((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β π β βͺ π¦) |
184 | 183 | neneqd 2945 |
. . 3
β’ ((π β§ π¦ β (π« (π΅ β πΉ) β© Fin)) β Β¬ π = βͺ π¦) |
185 | 184 | nrexdv 3143 |
. 2
β’ (π β Β¬ βπ¦ β (π« (π΅ β πΉ) β© Fin)π = βͺ π¦) |
186 | 117, 185 | pm2.65i 193 |
1
β’ Β¬
π |