Step | Hyp | Ref
| Expression |
1 | | climexp.4 |
. . . 4
β’ π =
(β€β₯βπ) |
2 | | climexp.5 |
. . . 4
β’ (π β π β β€) |
3 | | climexp.8 |
. . . . . 6
β’ (π β π β
β0) |
4 | | eqid 2726 |
. . . . . . 7
β’
(TopOpenββfld) =
(TopOpenββfld) |
5 | 4 | expcn 24745 |
. . . . . 6
β’ (π β β0
β (π₯ β β
β¦ (π₯βπ)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
6 | 3, 5 | syl 17 |
. . . . 5
β’ (π β (π₯ β β β¦ (π₯βπ)) β
((TopOpenββfld) Cn
(TopOpenββfld))) |
7 | 4 | cncfcn1 24786 |
. . . . 5
β’
(ββcnββ) =
((TopOpenββfld) Cn
(TopOpenββfld)) |
8 | 6, 7 | eleqtrrdi 2838 |
. . . 4
β’ (π β (π₯ β β β¦ (π₯βπ)) β (ββcnββ)) |
9 | | climexp.6 |
. . . 4
β’ (π β πΉ:πβΆβ) |
10 | | climexp.7 |
. . . 4
β’ (π β πΉ β π΄) |
11 | | climcl 15449 |
. . . . 5
β’ (πΉ β π΄ β π΄ β β) |
12 | 10, 11 | syl 17 |
. . . 4
β’ (π β π΄ β β) |
13 | 1, 2, 8, 9, 10, 12 | climcncf 24775 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯βπ)) β πΉ) β ((π₯ β β β¦ (π₯βπ))βπ΄)) |
14 | | eqidd 2727 |
. . . 4
β’ (π β (π₯ β β β¦ (π₯βπ)) = (π₯ β β β¦ (π₯βπ))) |
15 | | simpr 484 |
. . . . 5
β’ ((π β§ π₯ = π΄) β π₯ = π΄) |
16 | 15 | oveq1d 7420 |
. . . 4
β’ ((π β§ π₯ = π΄) β (π₯βπ) = (π΄βπ)) |
17 | 12, 3 | expcld 14116 |
. . . 4
β’ (π β (π΄βπ) β β) |
18 | 14, 16, 12, 17 | fvmptd 6999 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯βπ))βπ΄) = (π΄βπ)) |
19 | 13, 18 | breqtrd 5167 |
. 2
β’ (π β ((π₯ β β β¦ (π₯βπ)) β πΉ) β (π΄βπ)) |
20 | | climexp.9 |
. . 3
β’ (π β π» β π) |
21 | | cnex 11193 |
. . . . 5
β’ β
β V |
22 | 21 | mptex 7220 |
. . . 4
β’ (π₯ β β β¦ (π₯βπ)) β V |
23 | 1 | fvexi 6899 |
. . . . 5
β’ π β V |
24 | | fex 7223 |
. . . . 5
β’ ((πΉ:πβΆβ β§ π β V) β πΉ β V) |
25 | 9, 23, 24 | sylancl 585 |
. . . 4
β’ (π β πΉ β V) |
26 | | coexg 7919 |
. . . 4
β’ (((π₯ β β β¦ (π₯βπ)) β V β§ πΉ β V) β ((π₯ β β β¦ (π₯βπ)) β πΉ) β V) |
27 | 22, 25, 26 | sylancr 586 |
. . 3
β’ (π β ((π₯ β β β¦ (π₯βπ)) β πΉ) β V) |
28 | | eqidd 2727 |
. . . . 5
β’ ((π β§ π β π) β (π₯ β β β¦ (π₯βπ)) = (π₯ β β β¦ (π₯βπ))) |
29 | | simpr 484 |
. . . . . 6
β’ (((π β§ π β π) β§ π₯ = (πΉβπ)) β π₯ = (πΉβπ)) |
30 | 29 | oveq1d 7420 |
. . . . 5
β’ (((π β§ π β π) β§ π₯ = (πΉβπ)) β (π₯βπ) = ((πΉβπ)βπ)) |
31 | 9 | ffvelcdmda 7080 |
. . . . 5
β’ ((π β§ π β π) β (πΉβπ) β β) |
32 | 3 | adantr 480 |
. . . . . 6
β’ ((π β§ π β π) β π β
β0) |
33 | 31, 32 | expcld 14116 |
. . . . 5
β’ ((π β§ π β π) β ((πΉβπ)βπ) β β) |
34 | 28, 30, 31, 33 | fvmptd 6999 |
. . . 4
β’ ((π β§ π β π) β ((π₯ β β β¦ (π₯βπ))β(πΉβπ)) = ((πΉβπ)βπ)) |
35 | | fvco3 6984 |
. . . . 5
β’ ((πΉ:πβΆβ β§ π β π) β (((π₯ β β β¦ (π₯βπ)) β πΉ)βπ) = ((π₯ β β β¦ (π₯βπ))β(πΉβπ))) |
36 | 9, 35 | sylan 579 |
. . . 4
β’ ((π β§ π β π) β (((π₯ β β β¦ (π₯βπ)) β πΉ)βπ) = ((π₯ β β β¦ (π₯βπ))β(πΉβπ))) |
37 | | climexp.1 |
. . . . . . 7
β’
β²ππ |
38 | | nfv 1909 |
. . . . . . 7
β’
β²π π β π |
39 | 37, 38 | nfan 1894 |
. . . . . 6
β’
β²π(π β§ π β π) |
40 | | climexp.3 |
. . . . . . . 8
β’
β²ππ» |
41 | | nfcv 2897 |
. . . . . . . 8
β’
β²ππ |
42 | 40, 41 | nffv 6895 |
. . . . . . 7
β’
β²π(π»βπ) |
43 | | climexp.2 |
. . . . . . . . 9
β’
β²ππΉ |
44 | 43, 41 | nffv 6895 |
. . . . . . . 8
β’
β²π(πΉβπ) |
45 | | nfcv 2897 |
. . . . . . . 8
β’
β²πβ |
46 | | nfcv 2897 |
. . . . . . . 8
β’
β²ππ |
47 | 44, 45, 46 | nfov 7435 |
. . . . . . 7
β’
β²π((πΉβπ)βπ) |
48 | 42, 47 | nfeq 2910 |
. . . . . 6
β’
β²π(π»βπ) = ((πΉβπ)βπ) |
49 | 39, 48 | nfim 1891 |
. . . . 5
β’
β²π((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) |
50 | | eleq1w 2810 |
. . . . . . 7
β’ (π = π β (π β π β π β π)) |
51 | 50 | anbi2d 628 |
. . . . . 6
β’ (π = π β ((π β§ π β π) β (π β§ π β π))) |
52 | | fveq2 6885 |
. . . . . . 7
β’ (π = π β (π»βπ) = (π»βπ)) |
53 | | fveq2 6885 |
. . . . . . . 8
β’ (π = π β (πΉβπ) = (πΉβπ)) |
54 | 53 | oveq1d 7420 |
. . . . . . 7
β’ (π = π β ((πΉβπ)βπ) = ((πΉβπ)βπ)) |
55 | 52, 54 | eqeq12d 2742 |
. . . . . 6
β’ (π = π β ((π»βπ) = ((πΉβπ)βπ) β (π»βπ) = ((πΉβπ)βπ))) |
56 | 51, 55 | imbi12d 344 |
. . . . 5
β’ (π = π β (((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) β ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)))) |
57 | | climexp.10 |
. . . . 5
β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) |
58 | 49, 56, 57 | chvarfv 2225 |
. . . 4
β’ ((π β§ π β π) β (π»βπ) = ((πΉβπ)βπ)) |
59 | 34, 36, 58 | 3eqtr4rd 2777 |
. . 3
β’ ((π β§ π β π) β (π»βπ) = (((π₯ β β β¦ (π₯βπ)) β πΉ)βπ)) |
60 | 1, 20, 27, 2, 59 | climeq 15517 |
. 2
β’ (π β (π» β (π΄βπ) β ((π₯ β β β¦ (π₯βπ)) β πΉ) β (π΄βπ))) |
61 | 19, 60 | mpbird 257 |
1
β’ (π β π» β (π΄βπ)) |