Step | Hyp | Ref
| Expression |
1 | | limccl 25392 |
. . . 4
β’ (πΉ limβ π΅) β
β |
2 | 1 | sseli 3979 |
. . 3
β’ (πΆ β (πΉ limβ π΅) β πΆ β β) |
3 | 2 | pm4.71ri 562 |
. 2
β’ (πΆ β (πΉ limβ π΅) β (πΆ β β β§ πΆ β (πΉ limβ π΅))) |
4 | | eqid 2733 |
. . . . . 6
β’ (πΎ βΎt (π΄ βͺ {π΅})) = (πΎ βΎt (π΄ βͺ {π΅})) |
5 | | ellimc2.k |
. . . . . 6
β’ πΎ =
(TopOpenββfld) |
6 | | eqid 2733 |
. . . . . 6
β’ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) = (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) |
7 | | limccl.f |
. . . . . 6
β’ (π β πΉ:π΄βΆβ) |
8 | | limccl.a |
. . . . . 6
β’ (π β π΄ β β) |
9 | | limccl.b |
. . . . . 6
β’ (π β π΅ β β) |
10 | 4, 5, 6, 7, 8, 9 | ellimc 25390 |
. . . . 5
β’ (π β (πΆ β (πΉ limβ π΅) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (((πΎ βΎt (π΄ βͺ {π΅})) CnP πΎ)βπ΅))) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β§ πΆ β β) β (πΆ β (πΉ limβ π΅) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (((πΎ βΎt (π΄ βͺ {π΅})) CnP πΎ)βπ΅))) |
12 | 5 | cnfldtopon 24299 |
. . . . . . 7
β’ πΎ β
(TopOnββ) |
13 | 9 | snssd 4813 |
. . . . . . . 8
β’ (π β {π΅} β β) |
14 | 8, 13 | unssd 4187 |
. . . . . . 7
β’ (π β (π΄ βͺ {π΅}) β β) |
15 | | resttopon 22665 |
. . . . . . 7
β’ ((πΎ β (TopOnββ)
β§ (π΄ βͺ {π΅}) β β) β
(πΎ βΎt
(π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅}))) |
16 | 12, 14, 15 | sylancr 588 |
. . . . . 6
β’ (π β (πΎ βΎt (π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅}))) |
17 | 16 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β β) β (πΎ βΎt (π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅}))) |
18 | 12 | a1i 11 |
. . . . 5
β’ ((π β§ πΆ β β) β πΎ β
(TopOnββ)) |
19 | | ssun2 4174 |
. . . . . . 7
β’ {π΅} β (π΄ βͺ {π΅}) |
20 | | snssg 4788 |
. . . . . . . 8
β’ (π΅ β β β (π΅ β (π΄ βͺ {π΅}) β {π΅} β (π΄ βͺ {π΅}))) |
21 | 9, 20 | syl 17 |
. . . . . . 7
β’ (π β (π΅ β (π΄ βͺ {π΅}) β {π΅} β (π΄ βͺ {π΅}))) |
22 | 19, 21 | mpbiri 258 |
. . . . . 6
β’ (π β π΅ β (π΄ βͺ {π΅})) |
23 | 22 | adantr 482 |
. . . . 5
β’ ((π β§ πΆ β β) β π΅ β (π΄ βͺ {π΅})) |
24 | | elun 4149 |
. . . . . . . 8
β’ (π§ β (π΄ βͺ {π΅}) β (π§ β π΄ β¨ π§ β {π΅})) |
25 | | velsn 4645 |
. . . . . . . . 9
β’ (π§ β {π΅} β π§ = π΅) |
26 | 25 | orbi2i 912 |
. . . . . . . 8
β’ ((π§ β π΄ β¨ π§ β {π΅}) β (π§ β π΄ β¨ π§ = π΅)) |
27 | 24, 26 | bitri 275 |
. . . . . . 7
β’ (π§ β (π΄ βͺ {π΅}) β (π§ β π΄ β¨ π§ = π΅)) |
28 | | simpllr 775 |
. . . . . . . 8
β’ ((((π β§ πΆ β β) β§ (π§ β π΄ β¨ π§ = π΅)) β§ π§ = π΅) β πΆ β β) |
29 | | pm5.61 1000 |
. . . . . . . . . 10
β’ (((π§ β π΄ β¨ π§ = π΅) β§ Β¬ π§ = π΅) β (π§ β π΄ β§ Β¬ π§ = π΅)) |
30 | 7 | ffvelcdmda 7087 |
. . . . . . . . . . 11
β’ ((π β§ π§ β π΄) β (πΉβπ§) β β) |
31 | 30 | ad2ant2r 746 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β) β§ (π§ β π΄ β§ Β¬ π§ = π΅)) β (πΉβπ§) β β) |
32 | 29, 31 | sylan2b 595 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ ((π§ β π΄ β¨ π§ = π΅) β§ Β¬ π§ = π΅)) β (πΉβπ§) β β) |
33 | 32 | anassrs 469 |
. . . . . . . 8
β’ ((((π β§ πΆ β β) β§ (π§ β π΄ β¨ π§ = π΅)) β§ Β¬ π§ = π΅) β (πΉβπ§) β β) |
34 | 28, 33 | ifclda 4564 |
. . . . . . 7
β’ (((π β§ πΆ β β) β§ (π§ β π΄ β¨ π§ = π΅)) β if(π§ = π΅, πΆ, (πΉβπ§)) β β) |
35 | 27, 34 | sylan2b 595 |
. . . . . 6
β’ (((π β§ πΆ β β) β§ π§ β (π΄ βͺ {π΅})) β if(π§ = π΅, πΆ, (πΉβπ§)) β β) |
36 | 35 | fmpttd 7115 |
. . . . 5
β’ ((π β§ πΆ β β) β (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))):(π΄ βͺ {π΅})βΆβ) |
37 | | iscnp 22741 |
. . . . . 6
β’ (((πΎ βΎt (π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅})) β§ πΎ β (TopOnββ) β§ π΅ β (π΄ βͺ {π΅})) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (((πΎ βΎt (π΄ βͺ {π΅})) CnP πΎ)βπ΅) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))):(π΄ βͺ {π΅})βΆβ β§ βπ’ β πΎ (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’))))) |
38 | 37 | baibd 541 |
. . . . 5
β’ ((((πΎ βΎt (π΄ βͺ {π΅})) β (TopOnβ(π΄ βͺ {π΅})) β§ πΎ β (TopOnββ) β§ π΅ β (π΄ βͺ {π΅})) β§ (π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))):(π΄ βͺ {π΅})βΆβ) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (((πΎ βΎt (π΄ βͺ {π΅})) CnP πΎ)βπ΅) β βπ’ β πΎ (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)))) |
39 | 17, 18, 23, 36, 38 | syl31anc 1374 |
. . . 4
β’ ((π β§ πΆ β β) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (((πΎ βΎt (π΄ βͺ {π΅})) CnP πΎ)βπ΅) β βπ’ β πΎ (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)))) |
40 | | iftrue 4535 |
. . . . . . . . . . 11
β’ (π§ = π΅ β if(π§ = π΅, πΆ, (πΉβπ§)) = πΆ) |
41 | 40, 6 | fvmptg 6997 |
. . . . . . . . . 10
β’ ((π΅ β (π΄ βͺ {π΅}) β§ πΆ β β) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) = πΆ) |
42 | 22, 41 | sylan 581 |
. . . . . . . . 9
β’ ((π β§ πΆ β β) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) = πΆ) |
43 | 42 | eleq1d 2819 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β πΆ β π’)) |
44 | 43 | imbi1d 342 |
. . . . . . 7
β’ ((π β§ πΆ β β) β ((((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)) β (πΆ β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)))) |
45 | 44 | adantr 482 |
. . . . . 6
β’ (((π β§ πΆ β β) β§ π’ β πΎ) β ((((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)) β (πΆ β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)))) |
46 | 5 | cnfldtop 24300 |
. . . . . . . . . . 11
β’ πΎ β Top |
47 | | cnex 11191 |
. . . . . . . . . . . . . 14
β’ β
β V |
48 | 47 | ssex 5322 |
. . . . . . . . . . . . 13
β’ ((π΄ βͺ {π΅}) β β β (π΄ βͺ {π΅}) β V) |
49 | 14, 48 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (π΄ βͺ {π΅}) β V) |
50 | 49 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β (π΄ βͺ {π΅}) β V) |
51 | | restval 17372 |
. . . . . . . . . . 11
β’ ((πΎ β Top β§ (π΄ βͺ {π΅}) β V) β (πΎ βΎt (π΄ βͺ {π΅})) = ran (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅})))) |
52 | 46, 50, 51 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β (πΎ βΎt (π΄ βͺ {π΅})) = ran (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅})))) |
53 | 52 | rexeqdv 3327 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β (βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’) β βπ£ β ran (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅})))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’))) |
54 | | vex 3479 |
. . . . . . . . . . . 12
β’ π€ β V |
55 | 54 | inex1 5318 |
. . . . . . . . . . 11
β’ (π€ β© (π΄ βͺ {π΅})) β V |
56 | 55 | rgenw 3066 |
. . . . . . . . . 10
β’
βπ€ β
πΎ (π€ β© (π΄ βͺ {π΅})) β V |
57 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅}))) = (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅}))) |
58 | | eleq2 2823 |
. . . . . . . . . . . 12
β’ (π£ = (π€ β© (π΄ βͺ {π΅})) β (π΅ β π£ β π΅ β (π€ β© (π΄ βͺ {π΅})))) |
59 | | imaeq2 6056 |
. . . . . . . . . . . . 13
β’ (π£ = (π€ β© (π΄ βͺ {π΅})) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) = ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅})))) |
60 | 59 | sseq1d 4014 |
. . . . . . . . . . . 12
β’ (π£ = (π€ β© (π΄ βͺ {π΅})) β (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’ β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’)) |
61 | 58, 60 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π£ = (π€ β© (π΄ βͺ {π΅})) β ((π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’) β (π΅ β (π€ β© (π΄ βͺ {π΅})) β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’))) |
62 | 57, 61 | rexrnmptw 7097 |
. . . . . . . . . 10
β’
(βπ€ β
πΎ (π€ β© (π΄ βͺ {π΅})) β V β (βπ£ β ran (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅})))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’) β βπ€ β πΎ (π΅ β (π€ β© (π΄ βͺ {π΅})) β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’))) |
63 | 56, 62 | mp1i 13 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β (βπ£ β ran (π€ β πΎ β¦ (π€ β© (π΄ βͺ {π΅})))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’) β βπ€ β πΎ (π΅ β (π€ β© (π΄ βͺ {π΅})) β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’))) |
64 | 22 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β π΅ β (π΄ βͺ {π΅})) |
65 | | elin 3965 |
. . . . . . . . . . . . 13
β’ (π΅ β (π€ β© (π΄ βͺ {π΅})) β (π΅ β π€ β§ π΅ β (π΄ βͺ {π΅}))) |
66 | 65 | rbaib 540 |
. . . . . . . . . . . 12
β’ (π΅ β (π΄ βͺ {π΅}) β (π΅ β (π€ β© (π΄ βͺ {π΅})) β π΅ β π€)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (π΅ β (π€ β© (π΄ βͺ {π΅})) β π΅ β π€)) |
68 | | simpllr 775 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β πΆ β β) |
69 | | fvex 6905 |
. . . . . . . . . . . . . . . . 17
β’ (πΉβπ§) β V |
70 | | ifexg 4578 |
. . . . . . . . . . . . . . . . 17
β’ ((πΆ β β β§ (πΉβπ§) β V) β if(π§ = π΅, πΆ, (πΉβπ§)) β V) |
71 | 68, 69, 70 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β if(π§ = π΅, πΆ, (πΉβπ§)) β V) |
72 | 71 | ralrimivw 3151 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β βπ§ β (π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β V) |
73 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’ (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) = (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) |
74 | 73 | fnmpt 6691 |
. . . . . . . . . . . . . . 15
β’
(βπ§ β
(π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β V β (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) Fn (π€ β© (π΄ βͺ {π΅}))) |
75 | 73 | fmpt 7110 |
. . . . . . . . . . . . . . . . 17
β’
(βπ§ β
(π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))):(π€ β© (π΄ βͺ {π΅}))βΆπ’) |
76 | | df-f 6548 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))):(π€ β© (π΄ βͺ {π΅}))βΆπ’ β ((π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) Fn (π€ β© (π΄ βͺ {π΅})) β§ ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’)) |
77 | 75, 76 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’
(βπ§ β
(π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β ((π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) Fn (π€ β© (π΄ βͺ {π΅})) β§ ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’)) |
78 | 77 | baib 537 |
. . . . . . . . . . . . . . 15
β’ ((π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) Fn (π€ β© (π΄ βͺ {π΅})) β (βπ§ β (π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’)) |
79 | 72, 74, 78 | 3syl 18 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (βπ§ β (π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’)) |
80 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β πΆ β π’) |
81 | | elinel2 4197 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β (π€ β© {π΅}) β π§ β {π΅}) |
82 | 25, 40 | sylbi 216 |
. . . . . . . . . . . . . . . . . . 19
β’ (π§ β {π΅} β if(π§ = π΅, πΆ, (πΉβπ§)) = πΆ) |
83 | 82 | eleq1d 2819 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β {π΅} β (if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β πΆ β π’)) |
84 | 81, 83 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β (π€ β© {π΅}) β (if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β πΆ β π’)) |
85 | 80, 84 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (π§ β (π€ β© {π΅}) β if(π§ = π΅, πΆ, (πΉβπ§)) β π’)) |
86 | 85 | ralrimiv 3146 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β βπ§ β (π€ β© {π΅})if(π§ = π΅, πΆ, (πΉβπ§)) β π’) |
87 | | undif1 4476 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π΄ β {π΅}) βͺ {π΅}) = (π΄ βͺ {π΅}) |
88 | 87 | ineq2i 4210 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β© ((π΄ β {π΅}) βͺ {π΅})) = (π€ β© (π΄ βͺ {π΅})) |
89 | | indi 4274 |
. . . . . . . . . . . . . . . . . . 19
β’ (π€ β© ((π΄ β {π΅}) βͺ {π΅})) = ((π€ β© (π΄ β {π΅})) βͺ (π€ β© {π΅})) |
90 | 88, 89 | eqtr3i 2763 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ β© (π΄ βͺ {π΅})) = ((π€ β© (π΄ β {π΅})) βͺ (π€ β© {π΅})) |
91 | 90 | raleqi 3324 |
. . . . . . . . . . . . . . . . 17
β’
(βπ§ β
(π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β βπ§ β ((π€ β© (π΄ β {π΅})) βͺ (π€ β© {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’) |
92 | | ralunb 4192 |
. . . . . . . . . . . . . . . . 17
β’
(βπ§ β
((π€ β© (π΄ β {π΅})) βͺ (π€ β© {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β (βπ§ β (π€ β© (π΄ β {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β§ βπ§ β (π€ β© {π΅})if(π§ = π΅, πΆ, (πΉβπ§)) β π’)) |
93 | 91, 92 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’
(βπ§ β
(π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β (βπ§ β (π€ β© (π΄ β {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β§ βπ§ β (π€ β© {π΅})if(π§ = π΅, πΆ, (πΉβπ§)) β π’)) |
94 | 93 | rbaib 540 |
. . . . . . . . . . . . . . 15
β’
(βπ§ β
(π€ β© {π΅})if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β (βπ§ β (π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’)) |
95 | 86, 94 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (βπ§ β (π€ β© (π΄ βͺ {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’)) |
96 | 79, 95 | bitr3d 281 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’)) |
97 | | elinel2 4197 |
. . . . . . . . . . . . . . 15
β’ (π§ β (π€ β© (π΄ β {π΅})) β π§ β (π΄ β {π΅})) |
98 | | eldifsni 4794 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β (π΄ β {π΅}) β π§ β π΅) |
99 | | ifnefalse 4541 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β π΅ β if(π§ = π΅, πΆ, (πΉβπ§)) = (πΉβπ§)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π§ β (π΄ β {π΅}) β if(π§ = π΅, πΆ, (πΉβπ§)) = (πΉβπ§)) |
101 | 100 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π§ β (π΄ β {π΅}) β (if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β (πΉβπ§) β π’)) |
102 | 97, 101 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π§ β (π€ β© (π΄ β {π΅})) β (if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β (πΉβπ§) β π’)) |
103 | 102 | ralbiia 3092 |
. . . . . . . . . . . . 13
β’
(βπ§ β
(π€ β© (π΄ β {π΅}))if(π§ = π΅, πΆ, (πΉβπ§)) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))(πΉβπ§) β π’) |
104 | 96, 103 | bitrdi 287 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))(πΉβπ§) β π’)) |
105 | | df-ima 5690 |
. . . . . . . . . . . . . 14
β’ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) = ran ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) βΎ (π€ β© (π΄ βͺ {π΅}))) |
106 | | inss2 4230 |
. . . . . . . . . . . . . . . 16
β’ (π€ β© (π΄ βͺ {π΅})) β (π΄ βͺ {π΅}) |
107 | | resmpt 6038 |
. . . . . . . . . . . . . . . 16
β’ ((π€ β© (π΄ βͺ {π΅})) β (π΄ βͺ {π΅}) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) βΎ (π€ β© (π΄ βͺ {π΅}))) = (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))) |
108 | 106, 107 | mp1i 13 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) βΎ (π€ β© (π΄ βͺ {π΅}))) = (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))) |
109 | 108 | rneqd 5938 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β ran ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) βΎ (π€ β© (π΄ βͺ {π΅}))) = ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))) |
110 | 105, 109 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) = ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))) |
111 | 110 | sseq1d 4014 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’ β ran (π§ β (π€ β© (π΄ βͺ {π΅})) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π’)) |
112 | 7 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β πΉ:π΄βΆβ) |
113 | 112 | ffund 6722 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β Fun πΉ) |
114 | | inss2 4230 |
. . . . . . . . . . . . . . 15
β’ (π€ β© (π΄ β {π΅})) β (π΄ β {π΅}) |
115 | | difss 4132 |
. . . . . . . . . . . . . . 15
β’ (π΄ β {π΅}) β π΄ |
116 | 114, 115 | sstri 3992 |
. . . . . . . . . . . . . 14
β’ (π€ β© (π΄ β {π΅})) β π΄ |
117 | 112 | fdmd 6729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β dom πΉ = π΄) |
118 | 116, 117 | sseqtrrid 4036 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (π€ β© (π΄ β {π΅})) β dom πΉ) |
119 | | funimass4 6957 |
. . . . . . . . . . . . 13
β’ ((Fun
πΉ β§ (π€ β© (π΄ β {π΅})) β dom πΉ) β ((πΉ β (π€ β© (π΄ β {π΅}))) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))(πΉβπ§) β π’)) |
120 | 113, 118,
119 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β ((πΉ β (π€ β© (π΄ β {π΅}))) β π’ β βπ§ β (π€ β© (π΄ β {π΅}))(πΉβπ§) β π’)) |
121 | 104, 111,
120 | 3bitr4d 311 |
. . . . . . . . . . 11
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’ β (πΉ β (π€ β© (π΄ β {π΅}))) β π’)) |
122 | 67, 121 | anbi12d 632 |
. . . . . . . . . 10
β’ ((((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β§ π€ β πΎ) β ((π΅ β (π€ β© (π΄ βͺ {π΅})) β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’) β (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’))) |
123 | 122 | rexbidva 3177 |
. . . . . . . . 9
β’ (((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β (βπ€ β πΎ (π΅ β (π€ β© (π΄ βͺ {π΅})) β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β (π€ β© (π΄ βͺ {π΅}))) β π’) β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’))) |
124 | 53, 63, 123 | 3bitrd 305 |
. . . . . . . 8
β’ (((π β§ πΆ β β) β§ (π’ β πΎ β§ πΆ β π’)) β (βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’) β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’))) |
125 | 124 | anassrs 469 |
. . . . . . 7
β’ ((((π β§ πΆ β β) β§ π’ β πΎ) β§ πΆ β π’) β (βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’) β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’))) |
126 | 125 | pm5.74da 803 |
. . . . . 6
β’ (((π β§ πΆ β β) β§ π’ β πΎ) β ((πΆ β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)) β (πΆ β π’ β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’)))) |
127 | 45, 126 | bitrd 279 |
. . . . 5
β’ (((π β§ πΆ β β) β§ π’ β πΎ) β ((((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)) β (πΆ β π’ β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’)))) |
128 | 127 | ralbidva 3176 |
. . . 4
β’ ((π β§ πΆ β β) β (βπ’ β πΎ (((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§)))βπ΅) β π’ β βπ£ β (πΎ βΎt (π΄ βͺ {π΅}))(π΅ β π£ β§ ((π§ β (π΄ βͺ {π΅}) β¦ if(π§ = π΅, πΆ, (πΉβπ§))) β π£) β π’)) β βπ’ β πΎ (πΆ β π’ β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’)))) |
129 | 11, 39, 128 | 3bitrd 305 |
. . 3
β’ ((π β§ πΆ β β) β (πΆ β (πΉ limβ π΅) β βπ’ β πΎ (πΆ β π’ β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’)))) |
130 | 129 | pm5.32da 580 |
. 2
β’ (π β ((πΆ β β β§ πΆ β (πΉ limβ π΅)) β (πΆ β β β§ βπ’ β πΎ (πΆ β π’ β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’))))) |
131 | 3, 130 | bitrid 283 |
1
β’ (π β (πΆ β (πΉ limβ π΅) β (πΆ β β β§ βπ’ β πΎ (πΆ β π’ β βπ€ β πΎ (π΅ β π€ β§ (πΉ β (π€ β© (π΄ β {π΅}))) β π’))))) |