Step | Hyp | Ref
| Expression |
1 | | limccl.f |
. . . . . . . 8
β’ (π β πΉ:π΄βΆβ) |
2 | 1 | fdmd 6728 |
. . . . . . 7
β’ (π β dom πΉ = π΄) |
3 | 2 | adantr 480 |
. . . . . 6
β’ ((π β§ π₯ β (πΉ limβ π΅)) β dom πΉ = π΄) |
4 | | limcrcl 25624 |
. . . . . . . 8
β’ (π₯ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
5 | 4 | adantl 481 |
. . . . . . 7
β’ ((π β§ π₯ β (πΉ limβ π΅)) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
6 | 5 | simp2d 1142 |
. . . . . 6
β’ ((π β§ π₯ β (πΉ limβ π΅)) β dom πΉ β β) |
7 | 3, 6 | eqsstrrd 4021 |
. . . . 5
β’ ((π β§ π₯ β (πΉ limβ π΅)) β π΄ β β) |
8 | 5 | simp3d 1143 |
. . . . 5
β’ ((π β§ π₯ β (πΉ limβ π΅)) β π΅ β β) |
9 | 7, 8 | jca 511 |
. . . 4
β’ ((π β§ π₯ β (πΉ limβ π΅)) β (π΄ β β β§ π΅ β β)) |
10 | 9 | ex 412 |
. . 3
β’ (π β (π₯ β (πΉ limβ π΅) β (π΄ β β β§ π΅ β β))) |
11 | | undif1 4475 |
. . . . . . 7
β’ ((π΄ β {π΅}) βͺ {π΅}) = (π΄ βͺ {π΅}) |
12 | | difss 4131 |
. . . . . . . . . . . 12
β’ (π΄ β {π΅}) β π΄ |
13 | | fssres 6757 |
. . . . . . . . . . . 12
β’ ((πΉ:π΄βΆβ β§ (π΄ β {π΅}) β π΄) β (πΉ βΎ (π΄ β {π΅})):(π΄ β {π΅})βΆβ) |
14 | 1, 12, 13 | sylancl 585 |
. . . . . . . . . . 11
β’ (π β (πΉ βΎ (π΄ β {π΅})):(π΄ β {π΅})βΆβ) |
15 | 14 | fdmd 6728 |
. . . . . . . . . 10
β’ (π β dom (πΉ βΎ (π΄ β {π΅})) = (π΄ β {π΅})) |
16 | 15 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β dom (πΉ βΎ (π΄ β {π΅})) = (π΄ β {π΅})) |
17 | | limcrcl 25624 |
. . . . . . . . . . 11
β’ (π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅) β ((πΉ βΎ (π΄ β {π΅})):dom (πΉ βΎ (π΄ β {π΅}))βΆβ β§ dom (πΉ βΎ (π΄ β {π΅})) β β β§ π΅ β β)) |
18 | 17 | adantl 481 |
. . . . . . . . . 10
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β ((πΉ βΎ (π΄ β {π΅})):dom (πΉ βΎ (π΄ β {π΅}))βΆβ β§ dom (πΉ βΎ (π΄ β {π΅})) β β β§ π΅ β β)) |
19 | 18 | simp2d 1142 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β dom (πΉ βΎ (π΄ β {π΅})) β β) |
20 | 16, 19 | eqsstrrd 4021 |
. . . . . . . 8
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β (π΄ β {π΅}) β β) |
21 | 18 | simp3d 1143 |
. . . . . . . . 9
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β π΅ β β) |
22 | 21 | snssd 4812 |
. . . . . . . 8
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β {π΅} β β) |
23 | 20, 22 | unssd 4186 |
. . . . . . 7
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β ((π΄ β {π΅}) βͺ {π΅}) β β) |
24 | 11, 23 | eqsstrrid 4031 |
. . . . . 6
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β (π΄ βͺ {π΅}) β β) |
25 | 24 | unssad 4187 |
. . . . 5
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β π΄ β β) |
26 | 25, 21 | jca 511 |
. . . 4
β’ ((π β§ π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) β (π΄ β β β§ π΅ β β)) |
27 | 26 | ex 412 |
. . 3
β’ (π β (π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅) β (π΄ β β β§ π΅ β β))) |
28 | | eqid 2731 |
. . . . . 6
β’
((TopOpenββfld) βΎt (π΄ βͺ {π΅})) = ((TopOpenββfld)
βΎt (π΄
βͺ {π΅})) |
29 | | eqid 2731 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
30 | | eqid 2731 |
. . . . . 6
β’ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) = (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) |
31 | 1 | adantr 480 |
. . . . . 6
β’ ((π β§ (π΄ β β β§ π΅ β β)) β πΉ:π΄βΆβ) |
32 | | simprl 768 |
. . . . . 6
β’ ((π β§ (π΄ β β β§ π΅ β β)) β π΄ β β) |
33 | | simprr 770 |
. . . . . 6
β’ ((π β§ (π΄ β β β§ π΅ β β)) β π΅ β β) |
34 | 28, 29, 30, 31, 32, 33 | ellimc 25623 |
. . . . 5
β’ ((π β§ (π΄ β β β§ π΅ β β)) β (π₯ β (πΉ limβ π΅) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) β
((((TopOpenββfld) βΎt (π΄ βͺ {π΅})) CnP
(TopOpenββfld))βπ΅))) |
35 | 11 | eqcomi 2740 |
. . . . . . 7
β’ (π΄ βͺ {π΅}) = ((π΄ β {π΅}) βͺ {π΅}) |
36 | 35 | oveq2i 7423 |
. . . . . 6
β’
((TopOpenββfld) βΎt (π΄ βͺ {π΅})) = ((TopOpenββfld)
βΎt ((π΄
β {π΅}) βͺ {π΅})) |
37 | 35 | mpteq1i 5244 |
. . . . . . 7
β’ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) = (π§ β ((π΄ β {π΅}) βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) |
38 | | elun 4148 |
. . . . . . . . 9
β’ (π§ β ((π΄ β {π΅}) βͺ {π΅}) β (π§ β (π΄ β {π΅}) β¨ π§ β {π΅})) |
39 | | velsn 4644 |
. . . . . . . . . . 11
β’ (π§ β {π΅} β π§ = π΅) |
40 | 39 | orbi2i 910 |
. . . . . . . . . 10
β’ ((π§ β (π΄ β {π΅}) β¨ π§ β {π΅}) β (π§ β (π΄ β {π΅}) β¨ π§ = π΅)) |
41 | | pm5.61 998 |
. . . . . . . . . . . 12
β’ (((π§ β (π΄ β {π΅}) β¨ π§ = π΅) β§ Β¬ π§ = π΅) β (π§ β (π΄ β {π΅}) β§ Β¬ π§ = π΅)) |
42 | | fvres 6910 |
. . . . . . . . . . . . 13
β’ (π§ β (π΄ β {π΅}) β ((πΉ βΎ (π΄ β {π΅}))βπ§) = (πΉβπ§)) |
43 | 42 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π§ β (π΄ β {π΅}) β§ Β¬ π§ = π΅) β ((πΉ βΎ (π΄ β {π΅}))βπ§) = (πΉβπ§)) |
44 | 41, 43 | sylbi 216 |
. . . . . . . . . . 11
β’ (((π§ β (π΄ β {π΅}) β¨ π§ = π΅) β§ Β¬ π§ = π΅) β ((πΉ βΎ (π΄ β {π΅}))βπ§) = (πΉβπ§)) |
45 | 44 | ifeq2da 4560 |
. . . . . . . . . 10
β’ ((π§ β (π΄ β {π΅}) β¨ π§ = π΅) β if(π§ = π΅, π₯, ((πΉ βΎ (π΄ β {π΅}))βπ§)) = if(π§ = π΅, π₯, (πΉβπ§))) |
46 | 40, 45 | sylbi 216 |
. . . . . . . . 9
β’ ((π§ β (π΄ β {π΅}) β¨ π§ β {π΅}) β if(π§ = π΅, π₯, ((πΉ βΎ (π΄ β {π΅}))βπ§)) = if(π§ = π΅, π₯, (πΉβπ§))) |
47 | 38, 46 | sylbi 216 |
. . . . . . . 8
β’ (π§ β ((π΄ β {π΅}) βͺ {π΅}) β if(π§ = π΅, π₯, ((πΉ βΎ (π΄ β {π΅}))βπ§)) = if(π§ = π΅, π₯, (πΉβπ§))) |
48 | 47 | mpteq2ia 5251 |
. . . . . . 7
β’ (π§ β ((π΄ β {π΅}) βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ (π΄ β {π΅}))βπ§))) = (π§ β ((π΄ β {π΅}) βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) |
49 | 37, 48 | eqtr4i 2762 |
. . . . . 6
β’ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) = (π§ β ((π΄ β {π΅}) βͺ {π΅}) β¦ if(π§ = π΅, π₯, ((πΉ βΎ (π΄ β {π΅}))βπ§))) |
50 | 14 | adantr 480 |
. . . . . 6
β’ ((π β§ (π΄ β β β§ π΅ β β)) β (πΉ βΎ (π΄ β {π΅})):(π΄ β {π΅})βΆβ) |
51 | 32 | ssdifssd 4142 |
. . . . . 6
β’ ((π β§ (π΄ β β β§ π΅ β β)) β (π΄ β {π΅}) β β) |
52 | 36, 29, 49, 50, 51, 33 | ellimc 25623 |
. . . . 5
β’ ((π β§ (π΄ β β β§ π΅ β β)) β (π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, π₯, (πΉβπ§))) β
((((TopOpenββfld) βΎt (π΄ βͺ {π΅})) CnP
(TopOpenββfld))βπ΅))) |
53 | 34, 52 | bitr4d 282 |
. . . 4
β’ ((π β§ (π΄ β β β§ π΅ β β)) β (π₯ β (πΉ limβ π΅) β π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅))) |
54 | 53 | ex 412 |
. . 3
β’ (π β ((π΄ β β β§ π΅ β β) β (π₯ β (πΉ limβ π΅) β π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅)))) |
55 | 10, 27, 54 | pm5.21ndd 379 |
. 2
β’ (π β (π₯ β (πΉ limβ π΅) β π₯ β ((πΉ βΎ (π΄ β {π΅})) limβ π΅))) |
56 | 55 | eqrdv 2729 |
1
β’ (π β (πΉ limβ π΅) = ((πΉ βΎ (π΄ β {π΅})) limβ π΅)) |