Step | Hyp | Ref
| Expression |
1 | | cnmptcom.3 |
. . . . . . . . 9
β’ (π β π½ β (TopOnβπ)) |
2 | | cnmptcom.4 |
. . . . . . . . 9
β’ (π β πΎ β (TopOnβπ)) |
3 | | txtopon 22965 |
. . . . . . . . 9
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
4 | 1, 2, 3 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π½ Γt πΎ) β (TopOnβ(π Γ π))) |
5 | | cnmptcom.6 |
. . . . . . . . . 10
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) |
6 | | cntop2 22615 |
. . . . . . . . . 10
β’ ((π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ) β πΏ β Top) |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
β’ (π β πΏ β Top) |
8 | | toptopon2 22290 |
. . . . . . . . 9
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
9 | 7, 8 | sylib 217 |
. . . . . . . 8
β’ (π β πΏ β (TopOnββͺ πΏ)) |
10 | | cnf2 22623 |
. . . . . . . 8
β’ (((π½ Γt πΎ) β (TopOnβ(π Γ π)) β§ πΏ β (TopOnββͺ πΏ)
β§ (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
11 | 4, 9, 5, 10 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
12 | | eqid 2733 |
. . . . . . . . 9
β’ (π₯ β π, π¦ β π β¦ π΄) = (π₯ β π, π¦ β π β¦ π΄) |
13 | 12 | fmpo 8004 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π π΄ β βͺ πΏ β (π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
14 | | ralcom 3271 |
. . . . . . . 8
β’
(βπ₯ β
π βπ¦ β π π΄ β βͺ πΏ β βπ¦ β π βπ₯ β π π΄ β βͺ πΏ) |
15 | 13, 14 | bitr3i 277 |
. . . . . . 7
β’ ((π₯ β π, π¦ β π β¦ π΄):(π Γ π)βΆβͺ πΏ β βπ¦ β π βπ₯ β π π΄ β βͺ πΏ) |
16 | 11, 15 | sylib 217 |
. . . . . 6
β’ (π β βπ¦ β π βπ₯ β π π΄ β βͺ πΏ) |
17 | | eqid 2733 |
. . . . . . 7
β’ (π¦ β π, π₯ β π β¦ π΄) = (π¦ β π, π₯ β π β¦ π΄) |
18 | 17 | fmpo 8004 |
. . . . . 6
β’
(βπ¦ β
π βπ₯ β π π΄ β βͺ πΏ β (π¦ β π, π₯ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
19 | 16, 18 | sylib 217 |
. . . . 5
β’ (π β (π¦ β π, π₯ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
20 | 19 | ffnd 6673 |
. . . 4
β’ (π β (π¦ β π, π₯ β π β¦ π΄) Fn (π Γ π)) |
21 | | fnov 7491 |
. . . 4
β’ ((π¦ β π, π₯ β π β¦ π΄) Fn (π Γ π) β (π¦ β π, π₯ β π β¦ π΄) = (π§ β π, π€ β π β¦ (π§(π¦ β π, π₯ β π β¦ π΄)π€))) |
22 | 20, 21 | sylib 217 |
. . 3
β’ (π β (π¦ β π, π₯ β π β¦ π΄) = (π§ β π, π€ β π β¦ (π§(π¦ β π, π₯ β π β¦ π΄)π€))) |
23 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦π§ |
24 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯π§ |
25 | | nfcv 2904 |
. . . . . . 7
β’
β²π₯π€ |
26 | | nfv 1918 |
. . . . . . . 8
β’
β²π¦π |
27 | | nfcv 2904 |
. . . . . . . . . 10
β’
β²π¦π₯ |
28 | | nfmpo2 7442 |
. . . . . . . . . 10
β’
β²π¦(π₯ β π, π¦ β π β¦ π΄) |
29 | 27, 28, 23 | nfov 7391 |
. . . . . . . . 9
β’
β²π¦(π₯(π₯ β π, π¦ β π β¦ π΄)π§) |
30 | | nfmpo1 7441 |
. . . . . . . . . 10
β’
β²π¦(π¦ β π, π₯ β π β¦ π΄) |
31 | 23, 30, 27 | nfov 7391 |
. . . . . . . . 9
β’
β²π¦(π§(π¦ β π, π₯ β π β¦ π΄)π₯) |
32 | 29, 31 | nfeq 2917 |
. . . . . . . 8
β’
β²π¦(π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯) |
33 | 26, 32 | nfim 1900 |
. . . . . . 7
β’
β²π¦(π β (π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯)) |
34 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯π |
35 | | nfmpo1 7441 |
. . . . . . . . . 10
β’
β²π₯(π₯ β π, π¦ β π β¦ π΄) |
36 | 25, 35, 24 | nfov 7391 |
. . . . . . . . 9
β’
β²π₯(π€(π₯ β π, π¦ β π β¦ π΄)π§) |
37 | | nfmpo2 7442 |
. . . . . . . . . 10
β’
β²π₯(π¦ β π, π₯ β π β¦ π΄) |
38 | 24, 37, 25 | nfov 7391 |
. . . . . . . . 9
β’
β²π₯(π§(π¦ β π, π₯ β π β¦ π΄)π€) |
39 | 36, 38 | nfeq 2917 |
. . . . . . . 8
β’
β²π₯(π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€) |
40 | 34, 39 | nfim 1900 |
. . . . . . 7
β’
β²π₯(π β (π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€)) |
41 | | oveq2 7369 |
. . . . . . . . 9
β’ (π¦ = π§ β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = (π₯(π₯ β π, π¦ β π β¦ π΄)π§)) |
42 | | oveq1 7368 |
. . . . . . . . 9
β’ (π¦ = π§ β (π¦(π¦ β π, π₯ β π β¦ π΄)π₯) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯)) |
43 | 41, 42 | eqeq12d 2749 |
. . . . . . . 8
β’ (π¦ = π§ β ((π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = (π¦(π¦ β π, π₯ β π β¦ π΄)π₯) β (π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯))) |
44 | 43 | imbi2d 341 |
. . . . . . 7
β’ (π¦ = π§ β ((π β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = (π¦(π¦ β π, π₯ β π β¦ π΄)π₯)) β (π β (π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯)))) |
45 | | oveq1 7368 |
. . . . . . . . 9
β’ (π₯ = π€ β (π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π€(π₯ β π, π¦ β π β¦ π΄)π§)) |
46 | | oveq2 7369 |
. . . . . . . . 9
β’ (π₯ = π€ β (π§(π¦ β π, π₯ β π β¦ π΄)π₯) = (π§(π¦ β π, π₯ β π β¦ π΄)π€)) |
47 | 45, 46 | eqeq12d 2749 |
. . . . . . . 8
β’ (π₯ = π€ β ((π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯) β (π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€))) |
48 | 47 | imbi2d 341 |
. . . . . . 7
β’ (π₯ = π€ β ((π β (π₯(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π₯)) β (π β (π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€)))) |
49 | | rsp2 3259 |
. . . . . . . . 9
β’
(βπ¦ β
π βπ₯ β π π΄ β βͺ πΏ β ((π¦ β π β§ π₯ β π) β π΄ β βͺ πΏ)) |
50 | 49, 16 | syl11 33 |
. . . . . . . 8
β’ ((π¦ β π β§ π₯ β π) β (π β π΄ β βͺ πΏ)) |
51 | 12 | ovmpt4g 7506 |
. . . . . . . . . . 11
β’ ((π₯ β π β§ π¦ β π β§ π΄ β βͺ πΏ) β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = π΄) |
52 | 51 | 3com12 1124 |
. . . . . . . . . 10
β’ ((π¦ β π β§ π₯ β π β§ π΄ β βͺ πΏ) β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = π΄) |
53 | 17 | ovmpt4g 7506 |
. . . . . . . . . 10
β’ ((π¦ β π β§ π₯ β π β§ π΄ β βͺ πΏ) β (π¦(π¦ β π, π₯ β π β¦ π΄)π₯) = π΄) |
54 | 52, 53 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((π¦ β π β§ π₯ β π β§ π΄ β βͺ πΏ) β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = (π¦(π¦ β π, π₯ β π β¦ π΄)π₯)) |
55 | 54 | 3expia 1122 |
. . . . . . . 8
β’ ((π¦ β π β§ π₯ β π) β (π΄ β βͺ πΏ β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = (π¦(π¦ β π, π₯ β π β¦ π΄)π₯))) |
56 | 50, 55 | syld 47 |
. . . . . . 7
β’ ((π¦ β π β§ π₯ β π) β (π β (π₯(π₯ β π, π¦ β π β¦ π΄)π¦) = (π¦(π¦ β π, π₯ β π β¦ π΄)π₯))) |
57 | 23, 24, 25, 33, 40, 44, 48, 56 | vtocl2gaf 3538 |
. . . . . 6
β’ ((π§ β π β§ π€ β π) β (π β (π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€))) |
58 | 57 | com12 32 |
. . . . 5
β’ (π β ((π§ β π β§ π€ β π) β (π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€))) |
59 | 58 | 3impib 1117 |
. . . 4
β’ ((π β§ π§ β π β§ π€ β π) β (π€(π₯ β π, π¦ β π β¦ π΄)π§) = (π§(π¦ β π, π₯ β π β¦ π΄)π€)) |
60 | 59 | mpoeq3dva 7438 |
. . 3
β’ (π β (π§ β π, π€ β π β¦ (π€(π₯ β π, π¦ β π β¦ π΄)π§)) = (π§ β π, π€ β π β¦ (π§(π¦ β π, π₯ β π β¦ π΄)π€))) |
61 | 22, 60 | eqtr4d 2776 |
. 2
β’ (π β (π¦ β π, π₯ β π β¦ π΄) = (π§ β π, π€ β π β¦ (π€(π₯ β π, π¦ β π β¦ π΄)π§))) |
62 | 2, 1 | cnmpt2nd 23043 |
. . 3
β’ (π β (π§ β π, π€ β π β¦ π€) β ((πΎ Γt π½) Cn π½)) |
63 | 2, 1 | cnmpt1st 23042 |
. . 3
β’ (π β (π§ β π, π€ β π β¦ π§) β ((πΎ Γt π½) Cn πΎ)) |
64 | 2, 1, 62, 63, 5 | cnmpt22f 23049 |
. 2
β’ (π β (π§ β π, π€ β π β¦ (π€(π₯ β π, π¦ β π β¦ π΄)π§)) β ((πΎ Γt π½) Cn πΏ)) |
65 | 61, 64 | eqeltrd 2834 |
1
β’ (π β (π¦ β π, π₯ β π β¦ π΄) β ((πΎ Γt π½) Cn πΏ)) |