Step | Hyp | Ref
| Expression |
1 | | limcrcl 25261 |
. . . . . . 7
β’ (π₯ β (πΉ limβ π΅) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ π΅ β β)) |
2 | 1 | simp1d 1143 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β πΉ:dom πΉβΆβ) |
3 | 1 | simp2d 1144 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β dom πΉ β β) |
4 | 1 | simp3d 1145 |
. . . . . 6
β’ (π₯ β (πΉ limβ π΅) β π΅ β β) |
5 | | eqid 2733 |
. . . . . 6
β’
(TopOpenββfld) =
(TopOpenββfld) |
6 | 2, 3, 4, 5 | ellimc2 25264 |
. . . . 5
β’ (π₯ β (πΉ limβ π΅) β (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’))))) |
7 | 6 | ibi 267 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’)))) |
8 | | inss2 4193 |
. . . . . . . . . . . . 13
β’ (π£ β© ((dom πΉ β© πΆ) β {π΅})) β ((dom πΉ β© πΆ) β {π΅}) |
9 | | difss 4095 |
. . . . . . . . . . . . . 14
β’ ((dom
πΉ β© πΆ) β {π΅}) β (dom πΉ β© πΆ) |
10 | | inss2 4193 |
. . . . . . . . . . . . . 14
β’ (dom
πΉ β© πΆ) β πΆ |
11 | 9, 10 | sstri 3957 |
. . . . . . . . . . . . 13
β’ ((dom
πΉ β© πΆ) β {π΅}) β πΆ |
12 | 8, 11 | sstri 3957 |
. . . . . . . . . . . 12
β’ (π£ β© ((dom πΉ β© πΆ) β {π΅})) β πΆ |
13 | | resima2 5976 |
. . . . . . . . . . . 12
β’ ((π£ β© ((dom πΉ β© πΆ) β {π΅})) β πΆ β ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) = (πΉ β (π£ β© ((dom πΉ β© πΆ) β {π΅})))) |
14 | 12, 13 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) = (πΉ β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) |
15 | | inss1 4192 |
. . . . . . . . . . . . 13
β’ (dom
πΉ β© πΆ) β dom πΉ |
16 | | ssdif 4103 |
. . . . . . . . . . . . 13
β’ ((dom
πΉ β© πΆ) β dom πΉ β ((dom πΉ β© πΆ) β {π΅}) β (dom πΉ β {π΅})) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . . . . 12
β’ ((dom
πΉ β© πΆ) β {π΅}) β (dom πΉ β {π΅}) |
18 | | sslin 4198 |
. . . . . . . . . . . 12
β’ (((dom
πΉ β© πΆ) β {π΅}) β (dom πΉ β {π΅}) β (π£ β© ((dom πΉ β© πΆ) β {π΅})) β (π£ β© (dom πΉ β {π΅}))) |
19 | | imass2 6058 |
. . . . . . . . . . . 12
β’ ((π£ β© ((dom πΉ β© πΆ) β {π΅})) β (π£ β© (dom πΉ β {π΅})) β (πΉ β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β (πΉ β (π£ β© (dom πΉ β {π΅})))) |
20 | 17, 18, 19 | mp2b 10 |
. . . . . . . . . . 11
β’ (πΉ β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β (πΉ β (π£ β© (dom πΉ β {π΅}))) |
21 | 14, 20 | eqsstri 3982 |
. . . . . . . . . 10
β’ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β (πΉ β (π£ β© (dom πΉ β {π΅}))) |
22 | | sstr 3956 |
. . . . . . . . . 10
β’ ((((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β (πΉ β (π£ β© (dom πΉ β {π΅}))) β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’) β ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’) |
23 | 21, 22 | mpan 689 |
. . . . . . . . 9
β’ ((πΉ β (π£ β© (dom πΉ β {π΅}))) β π’ β ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’) |
24 | 23 | anim2i 618 |
. . . . . . . 8
β’ ((π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’) β (π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’)) |
25 | 24 | reximi 3084 |
. . . . . . 7
β’
(βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’) β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’)) |
26 | 25 | imim2i 16 |
. . . . . 6
β’ ((π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’)) β (π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’))) |
27 | 26 | ralimi 3083 |
. . . . 5
β’
(βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’)) β βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’))) |
28 | 27 | anim2i 618 |
. . . 4
β’ ((π₯ β β β§
βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ (πΉ β (π£ β© (dom πΉ β {π΅}))) β π’))) β (π₯ β β β§ βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’)))) |
29 | 7, 28 | syl 17 |
. . 3
β’ (π₯ β (πΉ limβ π΅) β (π₯ β β β§ βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’)))) |
30 | | fresin 6715 |
. . . . 5
β’ (πΉ:dom πΉβΆβ β (πΉ βΎ πΆ):(dom πΉ β© πΆ)βΆβ) |
31 | 2, 30 | syl 17 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (πΉ βΎ πΆ):(dom πΉ β© πΆ)βΆβ) |
32 | 15, 3 | sstrid 3959 |
. . . 4
β’ (π₯ β (πΉ limβ π΅) β (dom πΉ β© πΆ) β β) |
33 | 31, 32, 4, 5 | ellimc2 25264 |
. . 3
β’ (π₯ β (πΉ limβ π΅) β (π₯ β ((πΉ βΎ πΆ) limβ π΅) β (π₯ β β β§ βπ’ β
(TopOpenββfld)(π₯ β π’ β βπ£ β
(TopOpenββfld)(π΅ β π£ β§ ((πΉ βΎ πΆ) β (π£ β© ((dom πΉ β© πΆ) β {π΅}))) β π’))))) |
34 | 29, 33 | mpbird 257 |
. 2
β’ (π₯ β (πΉ limβ π΅) β π₯ β ((πΉ βΎ πΆ) limβ π΅)) |
35 | 34 | ssriv 3952 |
1
β’ (πΉ limβ π΅) β ((πΉ βΎ πΆ) limβ π΅) |