Step | Hyp | Ref
| Expression |
1 | | nfcv 2904 |
. . . . 5
β’
β²π₯π |
2 | | nfcv 2904 |
. . . . . 6
β’
β²π₯π£ |
3 | | nfmpo2 7442 |
. . . . . 6
β’
β²π₯(π¦ β π, π₯ β π β¦ π΄) |
4 | | nfcv 2904 |
. . . . . 6
β’
β²π₯π€ |
5 | 2, 3, 4 | nfov 7391 |
. . . . 5
β’
β²π₯(π£(π¦ β π, π₯ β π β¦ π΄)π€) |
6 | 1, 5 | nfmpt 5216 |
. . . 4
β’
β²π₯(π£ β π β¦ (π£(π¦ β π, π₯ β π β¦ π΄)π€)) |
7 | | nfcv 2904 |
. . . 4
β’
β²π€(π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π₯)) |
8 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦π£ |
9 | | nfmpo1 7441 |
. . . . . . 7
β’
β²π¦(π¦ β π, π₯ β π β¦ π΄) |
10 | | nfcv 2904 |
. . . . . . 7
β’
β²π¦π€ |
11 | 8, 9, 10 | nfov 7391 |
. . . . . 6
β’
β²π¦(π£(π¦ β π, π₯ β π β¦ π΄)π€) |
12 | | nfcv 2904 |
. . . . . 6
β’
β²π£(π¦(π¦ β π, π₯ β π β¦ π΄)π€) |
13 | | oveq1 7368 |
. . . . . 6
β’ (π£ = π¦ β (π£(π¦ β π, π₯ β π β¦ π΄)π€) = (π¦(π¦ β π, π₯ β π β¦ π΄)π€)) |
14 | 11, 12, 13 | cbvmpt 5220 |
. . . . 5
β’ (π£ β π β¦ (π£(π¦ β π, π₯ β π β¦ π΄)π€)) = (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π€)) |
15 | | oveq2 7369 |
. . . . . 6
β’ (π€ = π₯ β (π¦(π¦ β π, π₯ β π β¦ π΄)π€) = (π¦(π¦ β π, π₯ β π β¦ π΄)π₯)) |
16 | 15 | mpteq2dv 5211 |
. . . . 5
β’ (π€ = π₯ β (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π€)) = (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π₯))) |
17 | 14, 16 | eqtrid 2785 |
. . . 4
β’ (π€ = π₯ β (π£ β π β¦ (π£(π¦ β π, π₯ β π β¦ π΄)π€)) = (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π₯))) |
18 | 6, 7, 17 | cbvmpt 5220 |
. . 3
β’ (π€ β π β¦ (π£ β π β¦ (π£(π¦ β π, π₯ β π β¦ π΄)π€))) = (π₯ β π β¦ (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π₯))) |
19 | | simpr 486 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β π¦ β π) |
20 | | simplr 768 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β π₯ β π) |
21 | | cnmpt2k.k |
. . . . . . . . . . . 12
β’ (π β πΎ β (TopOnβπ)) |
22 | | cnmpt2k.j |
. . . . . . . . . . . 12
β’ (π β π½ β (TopOnβπ)) |
23 | | txtopon 22965 |
. . . . . . . . . . . 12
β’ ((πΎ β (TopOnβπ) β§ π½ β (TopOnβπ)) β (πΎ Γt π½) β (TopOnβ(π Γ π))) |
24 | 21, 22, 23 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β (πΎ Γt π½) β (TopOnβ(π Γ π))) |
25 | | cnmpt2k.a |
. . . . . . . . . . . . 13
β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) |
26 | | cntop2 22615 |
. . . . . . . . . . . . 13
β’ ((π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ) β πΏ β Top) |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
β’ (π β πΏ β Top) |
28 | | toptopon2 22290 |
. . . . . . . . . . . 12
β’ (πΏ β Top β πΏ β (TopOnββͺ πΏ)) |
29 | 27, 28 | sylib 217 |
. . . . . . . . . . 11
β’ (π β πΏ β (TopOnββͺ πΏ)) |
30 | 22, 21, 25 | cnmptcom 23052 |
. . . . . . . . . . 11
β’ (π β (π¦ β π, π₯ β π β¦ π΄) β ((πΎ Γt π½) Cn πΏ)) |
31 | | cnf2 22623 |
. . . . . . . . . . 11
β’ (((πΎ Γt π½) β (TopOnβ(π Γ π)) β§ πΏ β (TopOnββͺ πΏ)
β§ (π¦ β π, π₯ β π β¦ π΄) β ((πΎ Γt π½) Cn πΏ)) β (π¦ β π, π₯ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
32 | 24, 29, 30, 31 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π¦ β π, π₯ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
33 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π¦ β π, π₯ β π β¦ π΄) = (π¦ β π, π₯ β π β¦ π΄) |
34 | 33 | fmpo 8004 |
. . . . . . . . . 10
β’
(βπ¦ β
π βπ₯ β π π΄ β βͺ πΏ β (π¦ β π, π₯ β π β¦ π΄):(π Γ π)βΆβͺ πΏ) |
35 | 32, 34 | sylibr 233 |
. . . . . . . . 9
β’ (π β βπ¦ β π βπ₯ β π π΄ β βͺ πΏ) |
36 | 35 | r19.21bi 3233 |
. . . . . . . 8
β’ ((π β§ π¦ β π) β βπ₯ β π π΄ β βͺ πΏ) |
37 | 36 | r19.21bi 3233 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π₯ β π) β π΄ β βͺ πΏ) |
38 | 37 | an32s 651 |
. . . . . 6
β’ (((π β§ π₯ β π) β§ π¦ β π) β π΄ β βͺ πΏ) |
39 | 33 | ovmpt4g 7506 |
. . . . . 6
β’ ((π¦ β π β§ π₯ β π β§ π΄ β βͺ πΏ) β (π¦(π¦ β π, π₯ β π β¦ π΄)π₯) = π΄) |
40 | 19, 20, 38, 39 | syl3anc 1372 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π¦ β π) β (π¦(π¦ β π, π₯ β π β¦ π΄)π₯) = π΄) |
41 | 40 | mpteq2dva 5209 |
. . . 4
β’ ((π β§ π₯ β π) β (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π₯)) = (π¦ β π β¦ π΄)) |
42 | 41 | mpteq2dva 5209 |
. . 3
β’ (π β (π₯ β π β¦ (π¦ β π β¦ (π¦(π¦ β π, π₯ β π β¦ π΄)π₯))) = (π₯ β π β¦ (π¦ β π β¦ π΄))) |
43 | 18, 42 | eqtrid 2785 |
. 2
β’ (π β (π€ β π β¦ (π£ β π β¦ (π£(π¦ β π, π₯ β π β¦ π΄)π€))) = (π₯ β π β¦ (π¦ β π β¦ π΄))) |
44 | | eqid 2733 |
. . . . 5
β’ (π€ β π β¦ (π£ β π β¦ β¨π£, π€β©)) = (π€ β π β¦ (π£ β π β¦ β¨π£, π€β©)) |
45 | 44 | xkoinjcn 23061 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π€ β π β¦ (π£ β π β¦ β¨π£, π€β©)) β (π½ Cn ((πΎ Γt π½) βko πΎ))) |
46 | 22, 21, 45 | syl2anc 585 |
. . 3
β’ (π β (π€ β π β¦ (π£ β π β¦ β¨π£, π€β©)) β (π½ Cn ((πΎ Γt π½) βko πΎ))) |
47 | 32 | feqmptd 6914 |
. . . 4
β’ (π β (π¦ β π, π₯ β π β¦ π΄) = (π§ β (π Γ π) β¦ ((π¦ β π, π₯ β π β¦ π΄)βπ§))) |
48 | 47, 30 | eqeltrrd 2835 |
. . 3
β’ (π β (π§ β (π Γ π) β¦ ((π¦ β π, π₯ β π β¦ π΄)βπ§)) β ((πΎ Γt π½) Cn πΏ)) |
49 | | fveq2 6846 |
. . . 4
β’ (π§ = β¨π£, π€β© β ((π¦ β π, π₯ β π β¦ π΄)βπ§) = ((π¦ β π, π₯ β π β¦ π΄)ββ¨π£, π€β©)) |
50 | | df-ov 7364 |
. . . 4
β’ (π£(π¦ β π, π₯ β π β¦ π΄)π€) = ((π¦ β π, π₯ β π β¦ π΄)ββ¨π£, π€β©) |
51 | 49, 50 | eqtr4di 2791 |
. . 3
β’ (π§ = β¨π£, π€β© β ((π¦ β π, π₯ β π β¦ π΄)βπ§) = (π£(π¦ β π, π₯ β π β¦ π΄)π€)) |
52 | 22, 21, 24, 46, 48, 51 | cnmptk1 23055 |
. 2
β’ (π β (π€ β π β¦ (π£ β π β¦ (π£(π¦ β π, π₯ β π β¦ π΄)π€))) β (π½ Cn (πΏ βko πΎ))) |
53 | 43, 52 | eqeltrrd 2835 |
1
β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) |