Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π₯ β π) |
2 | | cnmptid.j |
. . . . . . . . . . 11
β’ (π β π½ β (TopOnβπ)) |
3 | | cnmpt11.k |
. . . . . . . . . . 11
β’ (π β πΎ β (TopOnβπ)) |
4 | | cnmpt11.a |
. . . . . . . . . . 11
β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) |
5 | | cnf2 22623 |
. . . . . . . . . . 11
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ (π₯ β π β¦ π΄) β (π½ Cn πΎ)) β (π₯ β π β¦ π΄):πβΆπ) |
6 | 2, 3, 4, 5 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π₯ β π β¦ π΄):πβΆπ) |
7 | 6 | fvmptelcdm 7065 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π΄ β π) |
8 | | eqid 2733 |
. . . . . . . . . 10
β’ (π₯ β π β¦ π΄) = (π₯ β π β¦ π΄) |
9 | 8 | fvmpt2 6963 |
. . . . . . . . 9
β’ ((π₯ β π β§ π΄ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
10 | 1, 7, 9 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ π΄)βπ₯) = π΄) |
11 | 10 | fveq2d 6850 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((π¦ β π β¦ π΅)β((π₯ β π β¦ π΄)βπ₯)) = ((π¦ β π β¦ π΅)βπ΄)) |
12 | | eqid 2733 |
. . . . . . . 8
β’ (π¦ β π β¦ π΅) = (π¦ β π β¦ π΅) |
13 | | cnmpt11.c |
. . . . . . . 8
β’ (π¦ = π΄ β π΅ = πΆ) |
14 | 13 | eleq1d 2819 |
. . . . . . . . 9
β’ (π¦ = π΄ β (π΅ β βͺ πΏ β πΆ β βͺ πΏ)) |
15 | | cnmpt11.b |
. . . . . . . . . . . . . 14
β’ (π β (π¦ β π β¦ π΅) β (πΎ Cn πΏ)) |
16 | | cntop2 22615 |
. . . . . . . . . . . . . 14
β’ ((π¦ β π β¦ π΅) β (πΎ Cn πΏ) β πΏ β Top) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β πΏ β Top) |
18 | | toptopon2 22290 |
. . . . . . . . . . . . 13
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
19 | 17, 18 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β πΏ β (TopOnββͺ πΏ)) |
20 | | cnf2 22623 |
. . . . . . . . . . . 12
β’ ((πΎ β (TopOnβπ) β§ πΏ β (TopOnββͺ πΏ)
β§ (π¦ β π β¦ π΅) β (πΎ Cn πΏ)) β (π¦ β π β¦ π΅):πβΆβͺ πΏ) |
21 | 3, 19, 15, 20 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β (π¦ β π β¦ π΅):πβΆβͺ πΏ) |
22 | 12 | fmpt 7062 |
. . . . . . . . . . 11
β’
(βπ¦ β
π π΅ β βͺ πΏ β (π¦ β π β¦ π΅):πβΆβͺ πΏ) |
23 | 21, 22 | sylibr 233 |
. . . . . . . . . 10
β’ (π β βπ¦ β π π΅ β βͺ πΏ) |
24 | 23 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β βπ¦ β π π΅ β βͺ πΏ) |
25 | 14, 24, 7 | rspcdva 3584 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β πΆ β βͺ πΏ) |
26 | 12, 13, 7, 25 | fvmptd3 6975 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((π¦ β π β¦ π΅)βπ΄) = πΆ) |
27 | 11, 26 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((π¦ β π β¦ π΅)β((π₯ β π β¦ π΄)βπ₯)) = πΆ) |
28 | | fvco3 6944 |
. . . . . . 7
β’ (((π₯ β π β¦ π΄):πβΆπ β§ π₯ β π) β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π¦ β π β¦ π΅)β((π₯ β π β¦ π΄)βπ₯))) |
29 | 6, 28 | sylan 581 |
. . . . . 6
β’ ((π β§ π₯ β π) β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π¦ β π β¦ π΅)β((π₯ β π β¦ π΄)βπ₯))) |
30 | | eqid 2733 |
. . . . . . . 8
β’ (π₯ β π β¦ πΆ) = (π₯ β π β¦ πΆ) |
31 | 30 | fvmpt2 6963 |
. . . . . . 7
β’ ((π₯ β π β§ πΆ β βͺ πΏ) β ((π₯ β π β¦ πΆ)βπ₯) = πΆ) |
32 | 1, 25, 31 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((π₯ β π β¦ πΆ)βπ₯) = πΆ) |
33 | 27, 29, 32 | 3eqtr4d 2783 |
. . . . 5
β’ ((π β§ π₯ β π) β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π₯ β π β¦ πΆ)βπ₯)) |
34 | 33 | ralrimiva 3140 |
. . . 4
β’ (π β βπ₯ β π (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π₯ β π β¦ πΆ)βπ₯)) |
35 | | nfv 1918 |
. . . . 5
β’
β²π§(((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π₯ β π β¦ πΆ)βπ₯) |
36 | | nfcv 2904 |
. . . . . . . 8
β’
β²π₯(π¦ β π β¦ π΅) |
37 | | nfmpt1 5217 |
. . . . . . . 8
β’
β²π₯(π₯ β π β¦ π΄) |
38 | 36, 37 | nfco 5825 |
. . . . . . 7
β’
β²π₯((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) |
39 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯π§ |
40 | 38, 39 | nffv 6856 |
. . . . . 6
β’
β²π₯(((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) |
41 | | nfmpt1 5217 |
. . . . . . 7
β’
β²π₯(π₯ β π β¦ πΆ) |
42 | 41, 39 | nffv 6856 |
. . . . . 6
β’
β²π₯((π₯ β π β¦ πΆ)βπ§) |
43 | 40, 42 | nfeq 2917 |
. . . . 5
β’
β²π₯(((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) = ((π₯ β π β¦ πΆ)βπ§) |
44 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π§ β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§)) |
45 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π§ β ((π₯ β π β¦ πΆ)βπ₯) = ((π₯ β π β¦ πΆ)βπ§)) |
46 | 44, 45 | eqeq12d 2749 |
. . . . 5
β’ (π₯ = π§ β ((((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π₯ β π β¦ πΆ)βπ₯) β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) = ((π₯ β π β¦ πΆ)βπ§))) |
47 | 35, 43, 46 | cbvralw 3288 |
. . . 4
β’
(βπ₯ β
π (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ₯) = ((π₯ β π β¦ πΆ)βπ₯) β βπ§ β π (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) = ((π₯ β π β¦ πΆ)βπ§)) |
48 | 34, 47 | sylib 217 |
. . 3
β’ (π β βπ§ β π (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) = ((π₯ β π β¦ πΆ)βπ§)) |
49 | | fco 6696 |
. . . . . 6
β’ (((π¦ β π β¦ π΅):πβΆβͺ πΏ β§ (π₯ β π β¦ π΄):πβΆπ) β ((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)):πβΆβͺ πΏ) |
50 | 21, 6, 49 | syl2anc 585 |
. . . . 5
β’ (π β ((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)):πβΆβͺ πΏ) |
51 | 50 | ffnd 6673 |
. . . 4
β’ (π β ((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) Fn π) |
52 | 25 | fmpttd 7067 |
. . . . 5
β’ (π β (π₯ β π β¦ πΆ):πβΆβͺ πΏ) |
53 | 52 | ffnd 6673 |
. . . 4
β’ (π β (π₯ β π β¦ πΆ) Fn π) |
54 | | eqfnfv 6986 |
. . . 4
β’ ((((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) Fn π β§ (π₯ β π β¦ πΆ) Fn π) β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) = (π₯ β π β¦ πΆ) β βπ§ β π (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) = ((π₯ β π β¦ πΆ)βπ§))) |
55 | 51, 53, 54 | syl2anc 585 |
. . 3
β’ (π β (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) = (π₯ β π β¦ πΆ) β βπ§ β π (((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄))βπ§) = ((π₯ β π β¦ πΆ)βπ§))) |
56 | 48, 55 | mpbird 257 |
. 2
β’ (π β ((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) = (π₯ β π β¦ πΆ)) |
57 | | cnco 22640 |
. . 3
β’ (((π₯ β π β¦ π΄) β (π½ Cn πΎ) β§ (π¦ β π β¦ π΅) β (πΎ Cn πΏ)) β ((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) β (π½ Cn πΏ)) |
58 | 4, 15, 57 | syl2anc 585 |
. 2
β’ (π β ((π¦ β π β¦ π΅) β (π₯ β π β¦ π΄)) β (π½ Cn πΏ)) |
59 | 56, 58 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) |