Step |
Hyp |
Ref |
Expression |
1 |
|
psrvsca.s |
โข ๐ = ( ๐ผ mPwSer ๐
) |
2 |
|
psrvsca.n |
โข โ = ( ยท๐ โ ๐ ) |
3 |
|
psrvsca.k |
โข ๐พ = ( Base โ ๐
) |
4 |
|
psrvsca.b |
โข ๐ต = ( Base โ ๐ ) |
5 |
|
psrvsca.m |
โข ยท = ( .r โ ๐
) |
6 |
|
psrvsca.d |
โข ๐ท = { โ โ ( โ0 โm ๐ผ ) โฃ ( โก โ โ โ ) โ Fin } |
7 |
|
eqid |
โข ( +g โ ๐
) = ( +g โ ๐
) |
8 |
|
eqid |
โข ( TopOpen โ ๐
) = ( TopOpen โ ๐
) |
9 |
|
simpl |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ ๐ผ โ V ) |
10 |
1 3 6 4 9
|
psrbas |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ ๐ต = ( ๐พ โm ๐ท ) ) |
11 |
|
eqid |
โข ( +g โ ๐ ) = ( +g โ ๐ ) |
12 |
1 4 7 11
|
psrplusg |
โข ( +g โ ๐ ) = ( โf ( +g โ ๐
) โพ ( ๐ต ร ๐ต ) ) |
13 |
|
eqid |
โข ( .r โ ๐ ) = ( .r โ ๐ ) |
14 |
1 4 5 13 6
|
psrmulr |
โข ( .r โ ๐ ) = ( ๐ โ ๐ต , ๐ โ ๐ต โฆ ( ๐ โ ๐ท โฆ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ยท ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) ) ) |
15 |
|
eqid |
โข ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) |
16 |
|
eqidd |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) = ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) ) |
17 |
|
simpr |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ ๐
โ V ) |
18 |
1 3 7 5 8 6 10 12 14 15 16 9 17
|
psrval |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ ๐ = ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) ) |
19 |
18
|
fveq2d |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ ( ยท๐ โ ๐ ) = ( ยท๐ โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) ) ) |
20 |
3
|
fvexi |
โข ๐พ โ V |
21 |
4
|
fvexi |
โข ๐ต โ V |
22 |
20 21
|
mpoex |
โข ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โ V |
23 |
|
psrvalstr |
โข ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) Struct โจ 1 , 9 โฉ |
24 |
|
vscaid |
โข ยท๐ = Slot ( ยท๐ โ ndx ) |
25 |
|
snsstp2 |
โข { โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ } โ { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } |
26 |
|
ssun2 |
โข { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) |
27 |
25 26
|
sstri |
โข { โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ } โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) |
28 |
23 24 27
|
strfv |
โข ( ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โ V โ ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) = ( ยท๐ โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) ) ) |
29 |
22 28
|
ax-mp |
โข ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) = ( ยท๐ โ ( { โจ ( Base โ ndx ) , ๐ต โฉ , โจ ( +g โ ndx ) , ( +g โ ๐ ) โฉ , โจ ( .r โ ndx ) , ( .r โ ๐ ) โฉ } โช { โจ ( Scalar โ ndx ) , ๐
โฉ , โจ ( ยท๐ โ ndx ) , ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) โฉ , โจ ( TopSet โ ndx ) , ( โt โ ( ๐ท ร { ( TopOpen โ ๐
) } ) ) โฉ } ) ) |
30 |
19 2 29
|
3eqtr4g |
โข ( ( ๐ผ โ V โง ๐
โ V ) โ โ = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) ) |
31 |
|
eqid |
โข โ
= โ
|
32 |
|
fn0 |
โข ( โ
Fn โ
โ โ
= โ
) |
33 |
31 32
|
mpbir |
โข โ
Fn โ
|
34 |
|
reldmpsr |
โข Rel dom mPwSer |
35 |
34
|
ovprc |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ๐ผ mPwSer ๐
) = โ
) |
36 |
1 35
|
eqtrid |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ๐ = โ
) |
37 |
36
|
fveq2d |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ยท๐ โ ๐ ) = ( ยท๐ โ โ
) ) |
38 |
24
|
str0 |
โข โ
= ( ยท๐ โ โ
) |
39 |
37 2 38
|
3eqtr4g |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ โ = โ
) |
40 |
34 1 4
|
elbasov |
โข ( ๐ โ ๐ต โ ( ๐ผ โ V โง ๐
โ V ) ) |
41 |
40
|
con3i |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ยฌ ๐ โ ๐ต ) |
42 |
41
|
eq0rdv |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ๐ต = โ
) |
43 |
42
|
xpeq2d |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ๐พ ร ๐ต ) = ( ๐พ ร โ
) ) |
44 |
|
xp0 |
โข ( ๐พ ร โ
) = โ
|
45 |
43 44
|
eqtrdi |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ๐พ ร ๐ต ) = โ
) |
46 |
39 45
|
fneq12d |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( โ Fn ( ๐พ ร ๐ต ) โ โ
Fn โ
) ) |
47 |
33 46
|
mpbiri |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ โ Fn ( ๐พ ร ๐ต ) ) |
48 |
|
fnov |
โข ( โ Fn ( ๐พ ร ๐ต ) โ โ = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ๐ฅ โ ๐ ) ) ) |
49 |
47 48
|
sylib |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ โ = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ๐ฅ โ ๐ ) ) ) |
50 |
41
|
pm2.21d |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ๐ โ ๐ต โ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) = ( ๐ฅ โ ๐ ) ) ) |
51 |
50
|
a1d |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ๐ฅ โ ๐พ โ ( ๐ โ ๐ต โ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) = ( ๐ฅ โ ๐ ) ) ) ) |
52 |
51
|
3imp |
โข ( ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โง ๐ฅ โ ๐พ โง ๐ โ ๐ต ) โ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) = ( ๐ฅ โ ๐ ) ) |
53 |
52
|
mpoeq3dva |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ๐ฅ โ ๐ ) ) ) |
54 |
49 53
|
eqtr4d |
โข ( ยฌ ( ๐ผ โ V โง ๐
โ V ) โ โ = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) ) |
55 |
30 54
|
pm2.61i |
โข โ = ( ๐ฅ โ ๐พ , ๐ โ ๐ต โฆ ( ( ๐ท ร { ๐ฅ } ) โf ยท ๐ ) ) |