Step | Hyp | Ref
| Expression |
1 | | breq2 4007 |
. . . . . . . . . 10
β’ (π = ((absβ(π₯ β π¦)) / 2) β ((absβ((πΉβπ§) β π₯)) < π β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2))) |
2 | 1 | imbi2d 230 |
. . . . . . . . 9
β’ (π = ((absβ(π₯ β π¦)) / 2) β (((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π) β ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) |
3 | 2 | rexralbidv 2503 |
. . . . . . . 8
β’ (π = ((absβ(π₯ β π¦)) / 2) β (βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) |
4 | | limcflf.f |
. . . . . . . . . . . . 13
β’ (π β πΉ:π΄βΆβ) |
5 | | limcflf.a |
. . . . . . . . . . . . 13
β’ (π β π΄ β β) |
6 | | limcimo.b |
. . . . . . . . . . . . 13
β’ (π β π΅ β β) |
7 | 4, 5, 6 | ellimc3ap 14066 |
. . . . . . . . . . . 12
β’ (π β (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π)))) |
8 | 7 | biimpa 296 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (πΉ limβ π΅)) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π))) |
9 | 8 | adantrr 479 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β (π₯ β β β§ βπ β β+
βπ β
β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π))) |
10 | 9 | simprd 114 |
. . . . . . . . 9
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π)) |
11 | 10 | adantr 276 |
. . . . . . . 8
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β βπ β β+ βπ β β+
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < π)) |
12 | 9 | simpld 112 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β π₯ β β) |
13 | 12 | adantr 276 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β π₯ β β) |
14 | 4, 5, 6 | ellimc3ap 14066 |
. . . . . . . . . . . . . . 15
β’ (π β (π¦ β (πΉ limβ π΅) β (π¦ β β β§ βπ β β+
βπ β
β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π)))) |
15 | 14 | biimpa 296 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (πΉ limβ π΅)) β (π¦ β β β§ βπ β β+
βπ β
β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π))) |
16 | 15 | adantrl 478 |
. . . . . . . . . . . . 13
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β (π¦ β β β§ βπ β β+
βπ β
β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π))) |
17 | 16 | simpld 112 |
. . . . . . . . . . . 12
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β π¦ β β) |
18 | 17 | adantr 276 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β π¦ β β) |
19 | 13, 18 | subcld 8267 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β (π₯ β π¦) β β) |
20 | | simpr 110 |
. . . . . . . . . . 11
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β π₯ # π¦) |
21 | 13, 18, 20 | subap0d 8600 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β (π₯ β π¦) # 0) |
22 | 19, 21 | absrpclapd 11196 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β (absβ(π₯ β π¦)) β
β+) |
23 | 22 | rphalfcld 9708 |
. . . . . . . 8
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β ((absβ(π₯ β π¦)) / 2) β
β+) |
24 | 3, 11, 23 | rspcdva 2846 |
. . . . . . 7
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β βπ β β+ βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2))) |
25 | | breq2 4007 |
. . . . . . . . . . . 12
β’ (π = ((absβ(π₯ β π¦)) / 2) β ((absβ((πΉβπ€) β π¦)) < π β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2))) |
26 | 25 | imbi2d 230 |
. . . . . . . . . . 11
β’ (π = ((absβ(π₯ β π¦)) / 2) β (((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π) β ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) |
27 | 26 | rexralbidv 2503 |
. . . . . . . . . 10
β’ (π = ((absβ(π₯ β π¦)) / 2) β (βπ β β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π) β βπ β β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) |
28 | 16 | simprd 114 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β βπ β β+ βπ β β+
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π)) |
29 | 28 | adantr 276 |
. . . . . . . . . 10
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β βπ β β+ βπ β β+
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < π)) |
30 | 27, 29, 23 | rspcdva 2846 |
. . . . . . . . 9
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β βπ β β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2))) |
31 | 30 | adantr 276 |
. . . . . . . 8
β’ ((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β βπ β β+ βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2))) |
32 | 4 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β πΉ:π΄βΆβ) |
33 | 5 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π΄ β β) |
34 | 6 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π΅ β β) |
35 | | limcimo.bc |
. . . . . . . . . 10
β’ (π β π΅ β πΆ) |
36 | 35 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π΅ β πΆ) |
37 | | limcimo.bs |
. . . . . . . . . 10
β’ (π β π΅ β π) |
38 | 37 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π΅ β π) |
39 | | limcimo.c |
. . . . . . . . . 10
β’ (π β πΆ β (πΎ βΎt π)) |
40 | 39 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β πΆ β (πΎ βΎt π)) |
41 | | limcimo.s |
. . . . . . . . . 10
β’ (π β π β {β, β}) |
42 | 41 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π β {β, β}) |
43 | | limcimo.ca |
. . . . . . . . . 10
β’ (π β {π β πΆ β£ π # π΅} β π΄) |
44 | 43 | ad4antr 494 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β {π β πΆ β£ π # π΅} β π΄) |
45 | | limcflfcntop.k |
. . . . . . . . 9
β’ πΎ = (MetOpenβ(abs β
β )) |
46 | | simplrl 535 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π β β+) |
47 | | simprl 529 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β π₯ β (πΉ limβ π΅)) |
48 | 47 | ad3antrrr 492 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π₯ β (πΉ limβ π΅)) |
49 | | simprr 531 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β π¦ β (πΉ limβ π΅)) |
50 | 49 | ad3antrrr 492 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π¦ β (πΉ limβ π΅)) |
51 | | simplrr 536 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2))) |
52 | | simprl 529 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β π β β+) |
53 | | simprr 531 |
. . . . . . . . 9
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2))) |
54 | 32, 33, 34, 36, 38, 40, 42, 44, 45, 46, 48, 50, 51, 52, 53 | limcimolemlt 14069 |
. . . . . . . 8
β’
(((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β§ (π β β+ β§
βπ€ β π΄ ((π€ # π΅ β§ (absβ(π€ β π΅)) < π) β (absβ((πΉβπ€) β π¦)) < ((absβ(π₯ β π¦)) / 2)))) β (absβ(π₯ β π¦)) < (absβ(π₯ β π¦))) |
55 | 31, 54 | rexlimddv 2599 |
. . . . . . 7
β’ ((((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β§ (π β β+ β§
βπ§ β π΄ ((π§ # π΅ β§ (absβ(π§ β π΅)) < π) β (absβ((πΉβπ§) β π₯)) < ((absβ(π₯ β π¦)) / 2)))) β (absβ(π₯ β π¦)) < (absβ(π₯ β π¦))) |
56 | 24, 55 | rexlimddv 2599 |
. . . . . 6
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β (absβ(π₯ β π¦)) < (absβ(π₯ β π¦))) |
57 | 22 | rpred 9695 |
. . . . . . 7
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β (absβ(π₯ β π¦)) β β) |
58 | 57 | ltnrd 8068 |
. . . . . 6
β’ (((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β§ π₯ # π¦) β Β¬ (absβ(π₯ β π¦)) < (absβ(π₯ β π¦))) |
59 | 56, 58 | pm2.65da 661 |
. . . . 5
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β Β¬ π₯ # π¦) |
60 | | apti 8578 |
. . . . . 6
β’ ((π₯ β β β§ π¦ β β) β (π₯ = π¦ β Β¬ π₯ # π¦)) |
61 | 12, 17, 60 | syl2anc 411 |
. . . . 5
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β (π₯ = π¦ β Β¬ π₯ # π¦)) |
62 | 59, 61 | mpbird 167 |
. . . 4
β’ ((π β§ (π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅))) β π₯ = π¦) |
63 | 62 | ex 115 |
. . 3
β’ (π β ((π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅)) β π₯ = π¦)) |
64 | 63 | alrimivv 1875 |
. 2
β’ (π β βπ₯βπ¦((π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅)) β π₯ = π¦)) |
65 | | eleq1w 2238 |
. . 3
β’ (π₯ = π¦ β (π₯ β (πΉ limβ π΅) β π¦ β (πΉ limβ π΅))) |
66 | 65 | mo4 2087 |
. 2
β’
(β*π₯ π₯ β (πΉ limβ π΅) β βπ₯βπ¦((π₯ β (πΉ limβ π΅) β§ π¦ β (πΉ limβ π΅)) β π₯ = π¦)) |
67 | 64, 66 | sylibr 134 |
1
β’ (π β β*π₯ π₯ β (πΉ limβ π΅)) |