Step | Hyp | Ref
| Expression |
1 | | limcrcl 25391 |
. . . . 5
β’ (π₯ β (πΉ limβ πΆ) β (πΉ:dom πΉβΆβ β§ dom πΉ β β β§ πΆ β β)) |
2 | 1 | simp3d 1145 |
. . . 4
β’ (π₯ β (πΉ limβ πΆ) β πΆ β β) |
3 | 2 | a1i 11 |
. . 3
β’ (π β (π₯ β (πΉ limβ πΆ) β πΆ β β)) |
4 | | elinel1 4196 |
. . . . 5
β’ (π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)) β π₯ β ((πΉ βΎ π΄) limβ πΆ)) |
5 | | limcrcl 25391 |
. . . . . 6
β’ (π₯ β ((πΉ βΎ π΄) limβ πΆ) β ((πΉ βΎ π΄):dom (πΉ βΎ π΄)βΆβ β§ dom (πΉ βΎ π΄) β β β§ πΆ β β)) |
6 | 5 | simp3d 1145 |
. . . . 5
β’ (π₯ β ((πΉ βΎ π΄) limβ πΆ) β πΆ β β) |
7 | 4, 6 | syl 17 |
. . . 4
β’ (π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)) β πΆ β β) |
8 | 7 | a1i 11 |
. . 3
β’ (π β (π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)) β πΆ β β)) |
9 | | prfi 9322 |
. . . . . . . 8
β’ {π΄, π΅} β Fin |
10 | 9 | a1i 11 |
. . . . . . 7
β’ ((π β§ πΆ β β) β {π΄, π΅} β Fin) |
11 | | limcun.1 |
. . . . . . . . 9
β’ (π β π΄ β β) |
12 | 11 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β π΄ β β) |
13 | | limcun.2 |
. . . . . . . . 9
β’ (π β π΅ β β) |
14 | 13 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β π΅ β β) |
15 | | cnex 11191 |
. . . . . . . . . . 11
β’ β
β V |
16 | 15 | ssex 5322 |
. . . . . . . . . 10
β’ (π΄ β β β π΄ β V) |
17 | 12, 16 | syl 17 |
. . . . . . . . 9
β’ ((π β§ πΆ β β) β π΄ β V) |
18 | 15 | ssex 5322 |
. . . . . . . . . 10
β’ (π΅ β β β π΅ β V) |
19 | 14, 18 | syl 17 |
. . . . . . . . 9
β’ ((π β§ πΆ β β) β π΅ β V) |
20 | | sseq1 4008 |
. . . . . . . . . 10
β’ (π¦ = π΄ β (π¦ β β β π΄ β β)) |
21 | | sseq1 4008 |
. . . . . . . . . 10
β’ (π¦ = π΅ β (π¦ β β β π΅ β β)) |
22 | 20, 21 | ralprg 4699 |
. . . . . . . . 9
β’ ((π΄ β V β§ π΅ β V) β (βπ¦ β {π΄, π΅}π¦ β β β (π΄ β β β§ π΅ β β))) |
23 | 17, 19, 22 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β (βπ¦ β {π΄, π΅}π¦ β β β (π΄ β β β§ π΅ β β))) |
24 | 12, 14, 23 | mpbir2and 712 |
. . . . . . 7
β’ ((π β§ πΆ β β) β βπ¦ β {π΄, π΅}π¦ β β) |
25 | | limcun.3 |
. . . . . . . . 9
β’ (π β πΉ:(π΄ βͺ π΅)βΆβ) |
26 | 25 | adantr 482 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β πΉ:(π΄ βͺ π΅)βΆβ) |
27 | | uniiun 5062 |
. . . . . . . . . 10
β’ βͺ {π΄,
π΅} = βͺ π¦ β {π΄, π΅}π¦ |
28 | | uniprg 4926 |
. . . . . . . . . . 11
β’ ((π΄ β V β§ π΅ β V) β βͺ {π΄,
π΅} = (π΄ βͺ π΅)) |
29 | 17, 19, 28 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ πΆ β β) β βͺ {π΄,
π΅} = (π΄ βͺ π΅)) |
30 | 27, 29 | eqtr3id 2787 |
. . . . . . . . 9
β’ ((π β§ πΆ β β) β βͺ π¦ β {π΄, π΅}π¦ = (π΄ βͺ π΅)) |
31 | 30 | feq2d 6704 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β (πΉ:βͺ π¦ β {π΄, π΅}π¦βΆβ β πΉ:(π΄ βͺ π΅)βΆβ)) |
32 | 26, 31 | mpbird 257 |
. . . . . . 7
β’ ((π β§ πΆ β β) β πΉ:βͺ π¦ β {π΄, π΅}π¦βΆβ) |
33 | | simpr 486 |
. . . . . . 7
β’ ((π β§ πΆ β β) β πΆ β β) |
34 | 10, 24, 32, 33 | limciun 25411 |
. . . . . 6
β’ ((π β§ πΆ β β) β (πΉ limβ πΆ) = (β β© β© π¦ β {π΄, π΅} ((πΉ βΎ π¦) limβ πΆ))) |
35 | 34 | eleq2d 2820 |
. . . . 5
β’ ((π β§ πΆ β β) β (π₯ β (πΉ limβ πΆ) β π₯ β (β β© β© π¦ β {π΄, π΅} ((πΉ βΎ π¦) limβ πΆ)))) |
36 | | reseq2 5977 |
. . . . . . . . . . . 12
β’ (π¦ = π΄ β (πΉ βΎ π¦) = (πΉ βΎ π΄)) |
37 | 36 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (π¦ = π΄ β ((πΉ βΎ π¦) limβ πΆ) = ((πΉ βΎ π΄) limβ πΆ)) |
38 | 37 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π¦ = π΄ β (π₯ β ((πΉ βΎ π¦) limβ πΆ) β π₯ β ((πΉ βΎ π΄) limβ πΆ))) |
39 | | reseq2 5977 |
. . . . . . . . . . . 12
β’ (π¦ = π΅ β (πΉ βΎ π¦) = (πΉ βΎ π΅)) |
40 | 39 | oveq1d 7424 |
. . . . . . . . . . 11
β’ (π¦ = π΅ β ((πΉ βΎ π¦) limβ πΆ) = ((πΉ βΎ π΅) limβ πΆ)) |
41 | 40 | eleq2d 2820 |
. . . . . . . . . 10
β’ (π¦ = π΅ β (π₯ β ((πΉ βΎ π¦) limβ πΆ) β π₯ β ((πΉ βΎ π΅) limβ πΆ))) |
42 | 38, 41 | ralprg 4699 |
. . . . . . . . 9
β’ ((π΄ β V β§ π΅ β V) β (βπ¦ β {π΄, π΅}π₯ β ((πΉ βΎ π¦) limβ πΆ) β (π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ)))) |
43 | 17, 19, 42 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ πΆ β β) β (βπ¦ β {π΄, π΅}π₯ β ((πΉ βΎ π¦) limβ πΆ) β (π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ)))) |
44 | 43 | anbi2d 630 |
. . . . . . 7
β’ ((π β§ πΆ β β) β ((π₯ β β β§ βπ¦ β {π΄, π΅}π₯ β ((πΉ βΎ π¦) limβ πΆ)) β (π₯ β β β§ (π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ))))) |
45 | | limccl 25392 |
. . . . . . . . . 10
β’ ((πΉ βΎ π΄) limβ πΆ) β β |
46 | 45 | sseli 3979 |
. . . . . . . . 9
β’ (π₯ β ((πΉ βΎ π΄) limβ πΆ) β π₯ β β) |
47 | 46 | adantr 482 |
. . . . . . . 8
β’ ((π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ)) β π₯ β β) |
48 | 47 | pm4.71ri 562 |
. . . . . . 7
β’ ((π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ)) β (π₯ β β β§ (π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ)))) |
49 | 44, 48 | bitr4di 289 |
. . . . . 6
β’ ((π β§ πΆ β β) β ((π₯ β β β§ βπ¦ β {π΄, π΅}π₯ β ((πΉ βΎ π¦) limβ πΆ)) β (π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ)))) |
50 | | elriin 5085 |
. . . . . 6
β’ (π₯ β (β β© β© π¦ β {π΄, π΅} ((πΉ βΎ π¦) limβ πΆ)) β (π₯ β β β§ βπ¦ β {π΄, π΅}π₯ β ((πΉ βΎ π¦) limβ πΆ))) |
51 | | elin 3965 |
. . . . . 6
β’ (π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)) β (π₯ β ((πΉ βΎ π΄) limβ πΆ) β§ π₯ β ((πΉ βΎ π΅) limβ πΆ))) |
52 | 49, 50, 51 | 3bitr4g 314 |
. . . . 5
β’ ((π β§ πΆ β β) β (π₯ β (β β© β© π¦ β {π΄, π΅} ((πΉ βΎ π¦) limβ πΆ)) β π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)))) |
53 | 35, 52 | bitrd 279 |
. . . 4
β’ ((π β§ πΆ β β) β (π₯ β (πΉ limβ πΆ) β π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)))) |
54 | 53 | ex 414 |
. . 3
β’ (π β (πΆ β β β (π₯ β (πΉ limβ πΆ) β π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ))))) |
55 | 3, 8, 54 | pm5.21ndd 381 |
. 2
β’ (π β (π₯ β (πΉ limβ πΆ) β π₯ β (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ)))) |
56 | 55 | eqrdv 2731 |
1
β’ (π β (πΉ limβ πΆ) = (((πΉ βΎ π΄) limβ πΆ) β© ((πΉ βΎ π΅) limβ πΆ))) |