Step | Hyp | Ref
| Expression |
1 | | df-ov 7412 |
. 2
β’ (π
ππ) = (πββ¨π
, πβ©) |
2 | | flfcnp2.j |
. . . . 5
β’ (π β π½ β (TopOnβπ)) |
3 | | flfcnp2.k |
. . . . 5
β’ (π β πΎ β (TopOnβπ)) |
4 | | txtopon 23095 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
5 | 2, 3, 4 | syl2anc 585 |
. . . 4
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
6 | | flfcnp2.l |
. . . 4
β’ (π β πΏ β (Filβπ)) |
7 | | flfcnp2.a |
. . . . . 6
β’ ((π β§ π₯ β π) β π΄ β π) |
8 | | flfcnp2.b |
. . . . . 6
β’ ((π β§ π₯ β π) β π΅ β π) |
9 | 7, 8 | opelxpd 5716 |
. . . . 5
β’ ((π β§ π₯ β π) β β¨π΄, π΅β© β (π Γ π)) |
10 | 9 | fmpttd 7115 |
. . . 4
β’ (π β (π₯ β π β¦ β¨π΄, π΅β©):πβΆ(π Γ π)) |
11 | | flfcnp2.r |
. . . . . 6
β’ (π β π
β ((π½ fLimf πΏ)β(π₯ β π β¦ π΄))) |
12 | | flfcnp2.s |
. . . . . 6
β’ (π β π β ((πΎ fLimf πΏ)β(π₯ β π β¦ π΅))) |
13 | 7 | fmpttd 7115 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΄):πβΆπ) |
14 | 8 | fmpttd 7115 |
. . . . . . 7
β’ (π β (π₯ β π β¦ π΅):πβΆπ) |
15 | | nfcv 2904 |
. . . . . . . 8
β’
β²π¦β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© |
16 | | nffvmpt1 6903 |
. . . . . . . . 9
β’
β²π₯((π₯ β π β¦ π΄)βπ¦) |
17 | | nffvmpt1 6903 |
. . . . . . . . 9
β’
β²π₯((π₯ β π β¦ π΅)βπ¦) |
18 | 16, 17 | nfop 4890 |
. . . . . . . 8
β’
β²π₯β¨((π₯ β π β¦ π΄)βπ¦), ((π₯ β π β¦ π΅)βπ¦)β© |
19 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((π₯ β π β¦ π΄)βπ₯) = ((π₯ β π β¦ π΄)βπ¦)) |
20 | | fveq2 6892 |
. . . . . . . . 9
β’ (π₯ = π¦ β ((π₯ β π β¦ π΅)βπ₯) = ((π₯ β π β¦ π΅)βπ¦)) |
21 | 19, 20 | opeq12d 4882 |
. . . . . . . 8
β’ (π₯ = π¦ β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨((π₯ β π β¦ π΄)βπ¦), ((π₯ β π β¦ π΅)βπ¦)β©) |
22 | 15, 18, 21 | cbvmpt 5260 |
. . . . . . 7
β’ (π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π¦ β π β¦ β¨((π₯ β π β¦ π΄)βπ¦), ((π₯ β π β¦ π΅)βπ¦)β©) |
23 | 2, 3, 6, 13, 14, 22 | txflf 23510 |
. . . . . 6
β’ (π β (β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)β(π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©)) β (π
β ((π½ fLimf πΏ)β(π₯ β π β¦ π΄)) β§ π β ((πΎ fLimf πΏ)β(π₯ β π β¦ π΅))))) |
24 | 11, 12, 23 | mpbir2and 712 |
. . . . 5
β’ (π β β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)β(π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©))) |
25 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π₯ β π) |
26 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
27 | 26 | fvmpt2 7010 |
. . . . . . . . 9
β’ ((π₯ β π β§ π΄ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
28 | 25, 7, 27 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
29 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π β¦ π΅) = (π₯ β π β¦ π΅) |
30 | 29 | fvmpt2 7010 |
. . . . . . . . 9
β’ ((π₯ β π β§ π΅ β π) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
31 | 25, 8, 30 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΅)βπ₯) = π΅) |
32 | 28, 31 | opeq12d 4882 |
. . . . . . 7
β’ ((π β§ π₯ β π) β β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β© = β¨π΄, π΅β©) |
33 | 32 | mpteq2dva 5249 |
. . . . . 6
β’ (π β (π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©) = (π₯ β π β¦ β¨π΄, π΅β©)) |
34 | 33 | fveq2d 6896 |
. . . . 5
β’ (π β (((π½ Γt πΎ) fLimf πΏ)β(π₯ β π β¦ β¨((π₯ β π β¦ π΄)βπ₯), ((π₯ β π β¦ π΅)βπ₯)β©)) = (((π½ Γt πΎ) fLimf πΏ)β(π₯ β π β¦ β¨π΄, π΅β©))) |
35 | 24, 34 | eleqtrd 2836 |
. . . 4
β’ (π β β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)β(π₯ β π β¦ β¨π΄, π΅β©))) |
36 | | flfcnp2.o |
. . . 4
β’ (π β π β (((π½ Γt πΎ) CnP π)ββ¨π
, πβ©)) |
37 | | flfcnp 23508 |
. . . 4
β’ ((((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ πΏ β (Filβπ) β§ (π₯ β π β¦ β¨π΄, π΅β©):πβΆ(π Γ π)) β§ (β¨π
, πβ© β (((π½ Γt πΎ) fLimf πΏ)β(π₯ β π β¦ β¨π΄, π΅β©)) β§ π β (((π½ Γt πΎ) CnP π)ββ¨π
, πβ©))) β (πββ¨π
, πβ©) β ((π fLimf πΏ)β(π β (π₯ β π β¦ β¨π΄, π΅β©)))) |
38 | 5, 6, 10, 35, 36, 37 | syl32anc 1379 |
. . 3
β’ (π β (πββ¨π
, πβ©) β ((π fLimf πΏ)β(π β (π₯ β π β¦ β¨π΄, π΅β©)))) |
39 | | eqidd 2734 |
. . . . 5
β’ (π β (π₯ β π β¦ β¨π΄, π΅β©) = (π₯ β π β¦ β¨π΄, π΅β©)) |
40 | | cnptop2 22747 |
. . . . . . . . 9
β’ (π β (((π½ Γt πΎ) CnP π)ββ¨π
, πβ©) β π β Top) |
41 | 36, 40 | syl 17 |
. . . . . . . 8
β’ (π β π β Top) |
42 | | toptopon2 22420 |
. . . . . . . 8
β’ (π β Top β π β (TopOnββͺ π)) |
43 | 41, 42 | sylib 217 |
. . . . . . 7
β’ (π β π β (TopOnββͺ π)) |
44 | | cnpf2 22754 |
. . . . . . 7
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ π β (TopOnββͺ π)
β§ π β (((π½ Γt πΎ) CnP π)ββ¨π
, πβ©)) β π:(π Γ π)βΆβͺ π) |
45 | 5, 43, 36, 44 | syl3anc 1372 |
. . . . . 6
β’ (π β π:(π Γ π)βΆβͺ π) |
46 | 45 | feqmptd 6961 |
. . . . 5
β’ (π β π = (π¦ β (π Γ π) β¦ (πβπ¦))) |
47 | | fveq2 6892 |
. . . . . 6
β’ (π¦ = β¨π΄, π΅β© β (πβπ¦) = (πββ¨π΄, π΅β©)) |
48 | | df-ov 7412 |
. . . . . 6
β’ (π΄ππ΅) = (πββ¨π΄, π΅β©) |
49 | 47, 48 | eqtr4di 2791 |
. . . . 5
β’ (π¦ = β¨π΄, π΅β© β (πβπ¦) = (π΄ππ΅)) |
50 | 9, 39, 46, 49 | fmptco 7127 |
. . . 4
β’ (π β (π β (π₯ β π β¦ β¨π΄, π΅β©)) = (π₯ β π β¦ (π΄ππ΅))) |
51 | 50 | fveq2d 6896 |
. . 3
β’ (π β ((π fLimf πΏ)β(π β (π₯ β π β¦ β¨π΄, π΅β©))) = ((π fLimf πΏ)β(π₯ β π β¦ (π΄ππ΅)))) |
52 | 38, 51 | eleqtrd 2836 |
. 2
β’ (π β (πββ¨π
, πβ©) β ((π fLimf πΏ)β(π₯ β π β¦ (π΄ππ΅)))) |
53 | 1, 52 | eqeltrid 2838 |
1
β’ (π β (π
ππ) β ((π fLimf πΏ)β(π₯ β π β¦ (π΄ππ΅)))) |