Step | Hyp | Ref
| Expression |
1 | | climexp.4 |
. . . 4
β’ π =
(β€β₯βπ) |
2 | | climexp.5 |
. . . 4
β’ (π β π β β€) |
3 | | climexp.8 |
. . . . . 6
β’ (π β π β
β0) |
4 | | eqid 2737 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
5 | 4 | expcn 24238 |
. . . . . 6
β’ (π β β0
β (π₯ β β
β¦ (π₯βπ)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
6 | 3, 5 | syl 17 |
. . . . 5
β’ (π β (π₯ β β β¦ (π₯βπ)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
7 | 4 | cncfcn1 24277 |
. . . . 5
β’
(ββcnββ) =
((TopOpenββfld) Cn
(TopOpenββfld)) |
8 | 6, 7 | eleqtrrdi 2849 |
. . . 4
β’ (π β (π₯ β β β¦ (π₯βπ)) β (ββcnββ)) |
9 | | climexp.6 |
. . . 4
β’ (π β πΉ:πβΆβ) |
10 | | climexp.7 |
. . . 4
β’ (π β πΉ β π΄) |
11 | | climcl 15382 |
. . . . 5
β’ (πΉ β π΄ β π΄ β β) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β π΄ β β) |
13 | 1, 2, 8, 9, 10, 12 | climcncf 24266 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯βπ)) β πΉ) β ((π₯ β β β¦ (π₯βπ))βπ΄)) |
14 | | eqidd 2738 |
. . . 4
β’ (π β (π₯ β β β¦ (π₯βπ)) = (π₯ β β β¦ (π₯βπ))) |
15 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ = π΄) β π₯ = π΄) |
16 | 15 | oveq1d 7373 |
. . . 4
β’ ((π β§ π₯ = π΄) β (π₯βπ) = (π΄βπ)) |
17 | 12, 3 | expcld 14052 |
. . . 4
β’ (π β (π΄βπ) β β) |
18 | 14, 16, 12, 17 | fvmptd 6956 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯βπ))βπ΄) = (π΄βπ)) |
19 | 13, 18 | breqtrd 5132 |
. 2
β’ (π β ((π₯ β β β¦ (π₯βπ)) β πΉ) β (π΄βπ)) |
20 | | climexp.9 |
. . 3
β’ (π β π» β π) |
21 | | cnex 11133 |
. . . . 5
β’ β
β V |
22 | 21 | mptex 7174 |
. . . 4
β’ (π₯ β β β¦ (π₯βπ)) β V |
23 | 1 | fvexi 6857 |
. . . . 5
β’ π β V |
24 | | fex 7177 |
. . . . 5
β’ ((πΉ:πβΆβ β§ π β V) β πΉ β V) |
25 | 9, 23, 24 | sylancl 587 |
. . . 4
β’ (π β πΉ β V) |
26 | | coexg 7867 |
. . . 4
β’ (((π₯ β β β¦ (π₯βπ)) β V β§ πΉ β V) β ((π₯ β β β¦ (π₯βπ)) β πΉ) β V) |
27 | 22, 25, 26 | sylancr 588 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯βπ)) β πΉ) β V) |
28 | | eqidd 2738 |
. . . . 5
β’ ((π β§ π β π) β (π₯ β β β¦ (π₯βπ)) = (π₯ β β β¦ (π₯βπ))) |
29 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β π) β§ π₯ = (πΉβπ)) β π₯ = (πΉβπ)) |
30 | 29 | oveq1d 7373 |
. . . . 5
β’ (((π β§ π β π) β§ π₯ = (πΉβπ)) β (π₯βπ) = ((πΉβπ)βπ)) |
31 | 9 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
32 | 3 | adantr 482 |
. . . . . 6
β’ ((π β§ π β π) β π β
β0) |
33 | 31, 32 | expcld 14052 |
. . . . 5
β’ ((π β§ π β π) β ((πΉβπ)βπ) β β) |
34 | 28, 30, 31, 33 | fvmptd 6956 |
. . . 4
β’ ((π β§ π β π) β ((π₯ β β β¦ (π₯βπ))β(πΉβπ)) = ((πΉβπ)βπ)) |
35 | | fvco3 6941 |
. . . . 5
β’ ((πΉ:πβΆβ β§ π β π) β (((π₯ β β β¦ (π₯βπ)) β πΉ)βπ) = ((π₯ β β β¦ (π₯βπ))β(πΉβπ))) |
36 | 9, 35 | sylan 581 |
. . . 4
β’ ((π β§ π β π) β (((π₯ β β β¦ (π₯βπ)) β πΉ)βπ) = ((π₯ β β β¦ (π₯βπ))β(πΉβπ))) |
37 | | climexp.1 |
. . . . . . 7
β’
β²ππ |
38 | | nfv 1918 |
. . . . . . 7
β’
β²π π β π |
39 | 37, 38 | nfan 1903 |
. . . . . 6
β’
β²π(π β§ π β π) |
40 | | climexp.3 |
. . . . . . . 8
β’
β²ππ» |
41 | | nfcv 2908 |
. . . . . . . 8
β’
β²ππ |
42 | 40, 41 | nffv 6853 |
. . . . . . 7
β’
β²π(π»βπ) |
43 | | climexp.2 |
. . . . . . . . 9
β’
β²ππΉ |
44 | 43, 41 | nffv 6853 |
. . . . . . . 8
β’
β²π(πΉβπ) |
45 | | nfcv 2908 |
. . . . . . . 8
β’
β²πβ |
46 | | nfcv 2908 |
. . . . . . . 8
β’
β²ππ |
47 | 44, 45, 46 | nfov 7388 |
. . . . . . 7
β’
β²π((πΉβπ)βπ) |
48 | 42, 47 | nfeq 2921 |
. . . . . 6
β’
β²π(π»βπ) = ((πΉβπ)βπ) |
49 | 39, 48 | nfim 1900 |
. . . . 5
β’
β²π((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) |
50 | | eleq1w 2821 |
. . . . . . 7
β’ (π = π β (π β π β π β π)) |
51 | 50 | anbi2d 630 |
. . . . . 6
β’ (π = π β ((π β§ π β π) β (π β§ π β π))) |
52 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (π»βπ) = (π»βπ)) |
53 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
54 | 53 | oveq1d 7373 |
. . . . . . 7
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
55 | 52, 54 | eqeq12d 2753 |
. . . . . 6
β’ (π = π β ((π»βπ) = ((πΉβπ)βπ) β (π»βπ) = ((πΉβπ)βπ))) |
56 | 51, 55 | imbi12d 345 |
. . . . 5
β’ (π = π β (((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) β ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)))) |
57 | | climexp.10 |
. . . . 5
β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) |
58 | 49, 56, 57 | chvarfv 2234 |
. . . 4
β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) |
59 | 34, 36, 58 | 3eqtr4rd 2788 |
. . 3
β’ ((π β§ π β π) β (π»βπ) = (((π₯ β β β¦ (π₯βπ)) β πΉ)βπ)) |
60 | 1, 20, 27, 2, 59 | climeq 15450 |
. 2
β’ (π β (π» β (π΄βπ) β ((π₯ β β β¦ (π₯βπ)) β πΉ) β (π΄βπ))) |
61 | 19, 60 | mpbird 257 |
1
β’ (π β π» β (π΄βπ)) |