Step | Hyp | Ref
| Expression |
1 | | noel 4331 |
. . . . . . . 8
β’ Β¬
π¦ β
β
|
2 | 1 | a1i 11 |
. . . . . . 7
β’ ((π β§ π΄ β dom (π D πΉ)) β Β¬ π¦ β β
) |
3 | | unbdqndv1.2 |
. . . . . . . . . . 11
β’ (π β π β π) |
4 | | unbdqndv1.1 |
. . . . . . . . . . 11
β’ (π β π β β) |
5 | 3, 4 | sstrd 3993 |
. . . . . . . . . 10
β’ (π β π β β) |
6 | 5 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π΄ β dom (π D πΉ)) β π β β) |
7 | 6 | ssdifssd 4143 |
. . . . . . . 8
β’ ((π β§ π΄ β dom (π D πΉ)) β (π β {π΄}) β β) |
8 | | unbdqndv1.3 |
. . . . . . . . . . 11
β’ (π β πΉ:πβΆβ) |
9 | 8 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π΄ β dom (π D πΉ)) β πΉ:πβΆβ) |
10 | 4, 8, 3 | dvbss 25651 |
. . . . . . . . . . 11
β’ (π β dom (π D πΉ) β π) |
11 | 10 | sselda 3983 |
. . . . . . . . . 10
β’ ((π β§ π΄ β dom (π D πΉ)) β π΄ β π) |
12 | 9, 6, 11 | dvlem 25646 |
. . . . . . . . 9
β’ (((π β§ π΄ β dom (π D πΉ)) β§ π§ β (π β {π΄})) β (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄)) β β) |
13 | | unbdqndv1.g |
. . . . . . . . 9
β’ πΊ = (π§ β (π β {π΄}) β¦ (((πΉβπ§) β (πΉβπ΄)) / (π§ β π΄))) |
14 | 12, 13 | fmptd 7116 |
. . . . . . . 8
β’ ((π β§ π΄ β dom (π D πΉ)) β πΊ:(π β {π΄})βΆβ) |
15 | 6, 11 | sseldd 3984 |
. . . . . . . 8
β’ ((π β§ π΄ β dom (π D πΉ)) β π΄ β β) |
16 | | unbdqndv1.4 |
. . . . . . . . 9
β’ (π β βπ β β+ βπ β β+
βπ₯ β (π β {π΄})((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΊβπ₯)))) |
17 | 16 | adantr 480 |
. . . . . . . 8
β’ ((π β§ π΄ β dom (π D πΉ)) β βπ β β+ βπ β β+
βπ₯ β (π β {π΄})((absβ(π₯ β π΄)) < π β§ π β€ (absβ(πΊβπ₯)))) |
18 | 7, 14, 15, 17 | unblimceq0 35687 |
. . . . . . 7
β’ ((π β§ π΄ β dom (π D πΉ)) β (πΊ limβ π΄) = β
) |
19 | 2, 18 | neleqtrrd 2855 |
. . . . . 6
β’ ((π β§ π΄ β dom (π D πΉ)) β Β¬ π¦ β (πΊ limβ π΄)) |
20 | 19 | intnand 488 |
. . . . 5
β’ ((π β§ π΄ β dom (π D πΉ)) β Β¬ (π΄ β
((intβ((TopOpenββfld) βΎt π))βπ) β§ π¦ β (πΊ limβ π΄))) |
21 | | eqid 2731 |
. . . . . . . 8
β’
((TopOpenββfld) βΎt π) =
((TopOpenββfld) βΎt π) |
22 | | eqid 2731 |
. . . . . . . 8
β’
(TopOpenββfld) =
(TopOpenββfld) |
23 | 21, 22, 13, 4, 8, 3 | eldv 25648 |
. . . . . . 7
β’ (π β (π΄(π D πΉ)π¦ β (π΄ β
((intβ((TopOpenββfld) βΎt π))βπ) β§ π¦ β (πΊ limβ π΄)))) |
24 | 23 | notbid 317 |
. . . . . 6
β’ (π β (Β¬ π΄(π D πΉ)π¦ β Β¬ (π΄ β
((intβ((TopOpenββfld) βΎt π))βπ) β§ π¦ β (πΊ limβ π΄)))) |
25 | 24 | adantr 480 |
. . . . 5
β’ ((π β§ π΄ β dom (π D πΉ)) β (Β¬ π΄(π D πΉ)π¦ β Β¬ (π΄ β
((intβ((TopOpenββfld) βΎt π))βπ) β§ π¦ β (πΊ limβ π΄)))) |
26 | 20, 25 | mpbird 256 |
. . . 4
β’ ((π β§ π΄ β dom (π D πΉ)) β Β¬ π΄(π D πΉ)π¦) |
27 | 26 | alrimiv 1929 |
. . 3
β’ ((π β§ π΄ β dom (π D πΉ)) β βπ¦ Β¬ π΄(π D πΉ)π¦) |
28 | | simpr 484 |
. . . . . 6
β’ ((π β§ π΄ β dom (π D πΉ)) β π΄ β dom (π D πΉ)) |
29 | | eldmg 5899 |
. . . . . 6
β’ (π΄ β dom (π D πΉ) β (π΄ β dom (π D πΉ) β βπ¦ π΄(π D πΉ)π¦)) |
30 | 28, 29 | syl 17 |
. . . . 5
β’ ((π β§ π΄ β dom (π D πΉ)) β (π΄ β dom (π D πΉ) β βπ¦ π΄(π D πΉ)π¦)) |
31 | 30 | notbid 317 |
. . . 4
β’ ((π β§ π΄ β dom (π D πΉ)) β (Β¬ π΄ β dom (π D πΉ) β Β¬ βπ¦ π΄(π D πΉ)π¦)) |
32 | | alnex 1782 |
. . . . . 6
β’
(βπ¦ Β¬
π΄(π D πΉ)π¦ β Β¬ βπ¦ π΄(π D πΉ)π¦) |
33 | 32 | a1i 11 |
. . . . 5
β’ ((π β§ π΄ β dom (π D πΉ)) β (βπ¦ Β¬ π΄(π D πΉ)π¦ β Β¬ βπ¦ π΄(π D πΉ)π¦)) |
34 | 33 | bicomd 222 |
. . . 4
β’ ((π β§ π΄ β dom (π D πΉ)) β (Β¬ βπ¦ π΄(π D πΉ)π¦ β βπ¦ Β¬ π΄(π D πΉ)π¦)) |
35 | 31, 34 | bitrd 278 |
. . 3
β’ ((π β§ π΄ β dom (π D πΉ)) β (Β¬ π΄ β dom (π D πΉ) β βπ¦ Β¬ π΄(π D πΉ)π¦)) |
36 | 27, 35 | mpbird 256 |
. 2
β’ ((π β§ π΄ β dom (π D πΉ)) β Β¬ π΄ β dom (π D πΉ)) |
37 | 36 | pm2.01da 796 |
1
β’ (π β Β¬ π΄ β dom (π D πΉ)) |