Step | Hyp | Ref
| Expression |
1 | | prdstmdd.y |
. . 3
β’ π = (πXsπ
) |
2 | | prdstmdd.i |
. . 3
β’ (π β πΌ β π) |
3 | | prdstmdd.s |
. . 3
β’ (π β π β π) |
4 | | prdstmdd.r |
. . . 4
β’ (π β π
:πΌβΆTopMnd) |
5 | | tmdmnd 23799 |
. . . . 5
β’ (π₯ β TopMnd β π₯ β Mnd) |
6 | 5 | ssriv 3985 |
. . . 4
β’ TopMnd
β Mnd |
7 | | fss 6733 |
. . . 4
β’ ((π
:πΌβΆTopMnd β§ TopMnd β Mnd)
β π
:πΌβΆMnd) |
8 | 4, 6, 7 | sylancl 584 |
. . 3
β’ (π β π
:πΌβΆMnd) |
9 | 1, 2, 3, 8 | prdsmndd 18692 |
. 2
β’ (π β π β Mnd) |
10 | | tmdtps 23800 |
. . . . 5
β’ (π₯ β TopMnd β π₯ β TopSp) |
11 | 10 | ssriv 3985 |
. . . 4
β’ TopMnd
β TopSp |
12 | | fss 6733 |
. . . 4
β’ ((π
:πΌβΆTopMnd β§ TopMnd β TopSp)
β π
:πΌβΆTopSp) |
13 | 4, 11, 12 | sylancl 584 |
. . 3
β’ (π β π
:πΌβΆTopSp) |
14 | 1, 3, 2, 13 | prdstps 23353 |
. 2
β’ (π β π β TopSp) |
15 | | eqid 2730 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
16 | 3 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β π β π) |
17 | 2 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β πΌ β π) |
18 | 4 | ffnd 6717 |
. . . . . . . 8
β’ (π β π
Fn πΌ) |
19 | 18 | 3ad2ant1 1131 |
. . . . . . 7
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β π
Fn πΌ) |
20 | | simp2 1135 |
. . . . . . 7
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β π β (Baseβπ)) |
21 | | simp3 1136 |
. . . . . . 7
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β π β (Baseβπ)) |
22 | | eqid 2730 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
23 | 1, 15, 16, 17, 19, 20, 21, 22 | prdsplusgval 17423 |
. . . . . 6
β’ ((π β§ π β (Baseβπ) β§ π β (Baseβπ)) β (π(+gβπ)π) = (π β πΌ β¦ ((πβπ)(+gβ(π
βπ))(πβπ)))) |
24 | 23 | mpoeq3dva 7488 |
. . . . 5
β’ (π β (π β (Baseβπ), π β (Baseβπ) β¦ (π(+gβπ)π)) = (π β (Baseβπ), π β (Baseβπ) β¦ (π β πΌ β¦ ((πβπ)(+gβ(π
βπ))(πβπ))))) |
25 | | eqid 2730 |
. . . . . 6
β’
(+πβπ) = (+πβπ) |
26 | 15, 22, 25 | plusffval 18571 |
. . . . 5
β’
(+πβπ) = (π β (Baseβπ), π β (Baseβπ) β¦ (π(+gβπ)π)) |
27 | | vex 3476 |
. . . . . . . . . 10
β’ π β V |
28 | | vex 3476 |
. . . . . . . . . 10
β’ π β V |
29 | 27, 28 | op1std 7987 |
. . . . . . . . 9
β’ (π§ = β¨π, πβ© β (1st βπ§) = π) |
30 | 29 | fveq1d 6892 |
. . . . . . . 8
β’ (π§ = β¨π, πβ© β ((1st βπ§)βπ) = (πβπ)) |
31 | 27, 28 | op2ndd 7988 |
. . . . . . . . 9
β’ (π§ = β¨π, πβ© β (2nd βπ§) = π) |
32 | 31 | fveq1d 6892 |
. . . . . . . 8
β’ (π§ = β¨π, πβ© β ((2nd βπ§)βπ) = (πβπ)) |
33 | 30, 32 | oveq12d 7429 |
. . . . . . 7
β’ (π§ = β¨π, πβ© β (((1st βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ)) = ((πβπ)(+gβ(π
βπ))(πβπ))) |
34 | 33 | mpteq2dv 5249 |
. . . . . 6
β’ (π§ = β¨π, πβ© β (π β πΌ β¦ (((1st βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ))) = (π β πΌ β¦ ((πβπ)(+gβ(π
βπ))(πβπ)))) |
35 | 34 | mpompt 7524 |
. . . . 5
β’ (π§ β ((Baseβπ) Γ (Baseβπ)) β¦ (π β πΌ β¦ (((1st βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ)))) = (π β (Baseβπ), π β (Baseβπ) β¦ (π β πΌ β¦ ((πβπ)(+gβ(π
βπ))(πβπ)))) |
36 | 24, 26, 35 | 3eqtr4g 2795 |
. . . 4
β’ (π β
(+πβπ) = (π§ β ((Baseβπ) Γ (Baseβπ)) β¦ (π β πΌ β¦ (((1st βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ))))) |
37 | | eqid 2730 |
. . . . 5
β’
(βtβ(TopOpen β π
)) = (βtβ(TopOpen
β π
)) |
38 | | eqid 2730 |
. . . . . . . 8
β’
(TopOpenβπ) =
(TopOpenβπ) |
39 | 15, 38 | istps 22656 |
. . . . . . 7
β’ (π β TopSp β
(TopOpenβπ) β
(TopOnβ(Baseβπ))) |
40 | 14, 39 | sylib 217 |
. . . . . 6
β’ (π β (TopOpenβπ) β
(TopOnβ(Baseβπ))) |
41 | | txtopon 23315 |
. . . . . 6
β’
(((TopOpenβπ)
β (TopOnβ(Baseβπ)) β§ (TopOpenβπ) β (TopOnβ(Baseβπ))) β ((TopOpenβπ) Γt
(TopOpenβπ)) β
(TopOnβ((Baseβπ) Γ (Baseβπ)))) |
42 | 40, 40, 41 | syl2anc 582 |
. . . . 5
β’ (π β ((TopOpenβπ) Γt
(TopOpenβπ)) β
(TopOnβ((Baseβπ) Γ (Baseβπ)))) |
43 | | topnfn 17375 |
. . . . . . . 8
β’ TopOpen
Fn V |
44 | | ssv 4005 |
. . . . . . . 8
β’ TopSp
β V |
45 | | fnssres 6672 |
. . . . . . . 8
β’ ((TopOpen
Fn V β§ TopSp β V) β (TopOpen βΎ TopSp) Fn
TopSp) |
46 | 43, 44, 45 | mp2an 688 |
. . . . . . 7
β’ (TopOpen
βΎ TopSp) Fn TopSp |
47 | | fvres 6909 |
. . . . . . . . 9
β’ (π₯ β TopSp β ((TopOpen
βΎ TopSp)βπ₯) =
(TopOpenβπ₯)) |
48 | | eqid 2730 |
. . . . . . . . . 10
β’
(TopOpenβπ₯) =
(TopOpenβπ₯) |
49 | 48 | tpstop 22659 |
. . . . . . . . 9
β’ (π₯ β TopSp β
(TopOpenβπ₯) β
Top) |
50 | 47, 49 | eqeltrd 2831 |
. . . . . . . 8
β’ (π₯ β TopSp β ((TopOpen
βΎ TopSp)βπ₯)
β Top) |
51 | 50 | rgen 3061 |
. . . . . . 7
β’
βπ₯ β
TopSp ((TopOpen βΎ TopSp)βπ₯) β Top |
52 | | ffnfv 7119 |
. . . . . . 7
β’ ((TopOpen
βΎ TopSp):TopSpβΆTop β ((TopOpen βΎ TopSp) Fn TopSp β§
βπ₯ β TopSp
((TopOpen βΎ TopSp)βπ₯) β Top)) |
53 | 46, 51, 52 | mpbir2an 707 |
. . . . . 6
β’ (TopOpen
βΎ TopSp):TopSpβΆTop |
54 | | fco2 6743 |
. . . . . 6
β’
(((TopOpen βΎ TopSp):TopSpβΆTop β§ π
:πΌβΆTopSp) β (TopOpen β π
):πΌβΆTop) |
55 | 53, 13, 54 | sylancr 585 |
. . . . 5
β’ (π β (TopOpen β π
):πΌβΆTop) |
56 | 33 | mpompt 7524 |
. . . . . 6
β’ (π§ β ((Baseβπ) Γ (Baseβπ)) β¦ (((1st
βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ))) = (π β (Baseβπ), π β (Baseβπ) β¦ ((πβπ)(+gβ(π
βπ))(πβπ))) |
57 | | eqid 2730 |
. . . . . . . 8
β’
(TopOpenβ(π
βπ)) = (TopOpenβ(π
βπ)) |
58 | | eqid 2730 |
. . . . . . . 8
β’
(+gβ(π
βπ)) = (+gβ(π
βπ)) |
59 | 4 | ffvelcdmda 7085 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (π
βπ) β TopMnd) |
60 | 40 | adantr 479 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (TopOpenβπ) β (TopOnβ(Baseβπ))) |
61 | 60, 60 | cnmpt1st 23392 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (π β (Baseβπ), π β (Baseβπ) β¦ π) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ))) |
62 | 1, 3, 2, 18, 38 | prdstopn 23352 |
. . . . . . . . . . . . . . 15
β’ (π β (TopOpenβπ) =
(βtβ(TopOpen β π
))) |
63 | 62 | adantr 479 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β πΌ) β (TopOpenβπ) = (βtβ(TopOpen
β π
))) |
64 | 63, 60 | eqeltrrd 2832 |
. . . . . . . . . . . . 13
β’ ((π β§ π β πΌ) β (βtβ(TopOpen
β π
)) β
(TopOnβ(Baseβπ))) |
65 | | toponuni 22636 |
. . . . . . . . . . . . 13
β’
((βtβ(TopOpen β π
)) β (TopOnβ(Baseβπ)) β (Baseβπ) = βͺ
(βtβ(TopOpen β π
))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β (Baseβπ) = βͺ
(βtβ(TopOpen β π
))) |
67 | 66 | mpteq1d 5242 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β (π₯ β (Baseβπ) β¦ (π₯βπ)) = (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ))) |
68 | 2 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β πΌ β π) |
69 | 55 | adantr 479 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β (TopOpen β π
):πΌβΆTop) |
70 | | simpr 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β πΌ) β π β πΌ) |
71 | | eqid 2730 |
. . . . . . . . . . . . 13
β’ βͺ (βtβ(TopOpen β π
)) = βͺ (βtβ(TopOpen β π
)) |
72 | 71, 37 | ptpjcn 23335 |
. . . . . . . . . . . 12
β’ ((πΌ β π β§ (TopOpen β π
):πΌβΆTop β§ π β πΌ) β (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ)) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ))) |
73 | 68, 69, 70, 72 | syl3anc 1369 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β (π₯ β βͺ
(βtβ(TopOpen β π
)) β¦ (π₯βπ)) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ))) |
74 | 67, 73 | eqeltrd 2831 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β (π₯ β (Baseβπ) β¦ (π₯βπ)) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ))) |
75 | 63 | eqcomd 2736 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β (βtβ(TopOpen
β π
)) =
(TopOpenβπ)) |
76 | | fvco3 6989 |
. . . . . . . . . . . 12
β’ ((π
:πΌβΆTopMnd β§ π β πΌ) β ((TopOpen β π
)βπ) = (TopOpenβ(π
βπ))) |
77 | 4, 76 | sylan 578 |
. . . . . . . . . . 11
β’ ((π β§ π β πΌ) β ((TopOpen β π
)βπ) = (TopOpenβ(π
βπ))) |
78 | 75, 77 | oveq12d 7429 |
. . . . . . . . . 10
β’ ((π β§ π β πΌ) β ((βtβ(TopOpen
β π
)) Cn ((TopOpen
β π
)βπ)) = ((TopOpenβπ) Cn (TopOpenβ(π
βπ)))) |
79 | 74, 78 | eleqtrd 2833 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (π₯ β (Baseβπ) β¦ (π₯βπ)) β ((TopOpenβπ) Cn (TopOpenβ(π
βπ)))) |
80 | | fveq1 6889 |
. . . . . . . . 9
β’ (π₯ = π β (π₯βπ) = (πβπ)) |
81 | 60, 60, 61, 60, 79, 80 | cnmpt21 23395 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (π β (Baseβπ), π β (Baseβπ) β¦ (πβπ)) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβ(π
βπ)))) |
82 | 60, 60 | cnmpt2nd 23393 |
. . . . . . . . 9
β’ ((π β§ π β πΌ) β (π β (Baseβπ), π β (Baseβπ) β¦ π) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ))) |
83 | | fveq1 6889 |
. . . . . . . . 9
β’ (π₯ = π β (π₯βπ) = (πβπ)) |
84 | 60, 60, 82, 60, 79, 83 | cnmpt21 23395 |
. . . . . . . 8
β’ ((π β§ π β πΌ) β (π β (Baseβπ), π β (Baseβπ) β¦ (πβπ)) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβ(π
βπ)))) |
85 | 57, 58, 59, 60, 60, 81, 84 | cnmpt2plusg 23812 |
. . . . . . 7
β’ ((π β§ π β πΌ) β (π β (Baseβπ), π β (Baseβπ) β¦ ((πβπ)(+gβ(π
βπ))(πβπ))) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβ(π
βπ)))) |
86 | 77 | oveq2d 7427 |
. . . . . . 7
β’ ((π β§ π β πΌ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn ((TopOpen β π
)βπ)) = (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβ(π
βπ)))) |
87 | 85, 86 | eleqtrrd 2834 |
. . . . . 6
β’ ((π β§ π β πΌ) β (π β (Baseβπ), π β (Baseβπ) β¦ ((πβπ)(+gβ(π
βπ))(πβπ))) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn ((TopOpen β π
)βπ))) |
88 | 56, 87 | eqeltrid 2835 |
. . . . 5
β’ ((π β§ π β πΌ) β (π§ β ((Baseβπ) Γ (Baseβπ)) β¦ (((1st βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ))) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn ((TopOpen β π
)βπ))) |
89 | 37, 42, 2, 55, 88 | ptcn 23351 |
. . . 4
β’ (π β (π§ β ((Baseβπ) Γ (Baseβπ)) β¦ (π β πΌ β¦ (((1st βπ§)βπ)(+gβ(π
βπ))((2nd βπ§)βπ)))) β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(βtβ(TopOpen β π
)))) |
90 | 36, 89 | eqeltrd 2831 |
. . 3
β’ (π β
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn
(βtβ(TopOpen β π
)))) |
91 | 62 | oveq2d 7427 |
. . 3
β’ (π β (((TopOpenβπ) Γt
(TopOpenβπ)) Cn
(TopOpenβπ)) =
(((TopOpenβπ)
Γt (TopOpenβπ)) Cn (βtβ(TopOpen
β π
)))) |
92 | 90, 91 | eleqtrrd 2834 |
. 2
β’ (π β
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ))) |
93 | 25, 38 | istmd 23798 |
. 2
β’ (π β TopMnd β (π β Mnd β§ π β TopSp β§
(+πβπ) β (((TopOpenβπ) Γt (TopOpenβπ)) Cn (TopOpenβπ)))) |
94 | 9, 14, 92, 93 | syl3anbrc 1341 |
1
β’ (π β π β TopMnd) |