Step | Hyp | Ref
| Expression |
1 | | opsrval.o |
. 2
β’ π = ((πΌ ordPwSer π
)βπ) |
2 | | opsrval.i |
. . . . 5
β’ (π β πΌ β π) |
3 | 2 | elexd 3464 |
. . . 4
β’ (π β πΌ β V) |
4 | | opsrval.r |
. . . . 5
β’ (π β π
β π) |
5 | 4 | elexd 3464 |
. . . 4
β’ (π β π
β V) |
6 | 2, 2 | xpexd 7676 |
. . . . 5
β’ (π β (πΌ Γ πΌ) β V) |
7 | | pwexg 5332 |
. . . . 5
β’ ((πΌ Γ πΌ) β V β π« (πΌ Γ πΌ) β V) |
8 | | mptexg 7166 |
. . . . 5
β’
(π« (πΌ
Γ πΌ) β V β
(π β π« (πΌ Γ πΌ) β¦ (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) β V) |
9 | 6, 7, 8 | 3syl 18 |
. . . 4
β’ (π β (π β π« (πΌ Γ πΌ) β¦ (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) β V) |
10 | | simpl 484 |
. . . . . . . 8
β’ ((π = πΌ β§ π = π
) β π = πΌ) |
11 | 10 | sqxpeqd 5663 |
. . . . . . 7
β’ ((π = πΌ β§ π = π
) β (π Γ π) = (πΌ Γ πΌ)) |
12 | 11 | pweqd 4576 |
. . . . . 6
β’ ((π = πΌ β§ π = π
) β π« (π Γ π) = π« (πΌ Γ πΌ)) |
13 | | ovexd 7385 |
. . . . . . 7
β’ ((π = πΌ β§ π = π
) β (π mPwSer π ) β V) |
14 | | id 22 |
. . . . . . . . . 10
β’ (π = (π mPwSer π ) β π = (π mPwSer π )) |
15 | | oveq12 7359 |
. . . . . . . . . 10
β’ ((π = πΌ β§ π = π
) β (π mPwSer π ) = (πΌ mPwSer π
)) |
16 | 14, 15 | sylan9eqr 2800 |
. . . . . . . . 9
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β π = (πΌ mPwSer π
)) |
17 | | opsrval.s |
. . . . . . . . 9
β’ π = (πΌ mPwSer π
) |
18 | 16, 17 | eqtr4di 2796 |
. . . . . . . 8
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β π = π) |
19 | 18 | fveq2d 6842 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β (Baseβπ) = (Baseβπ)) |
20 | | opsrval.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
21 | 19, 20 | eqtr4di 2796 |
. . . . . . . . . . . 12
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β (Baseβπ) = π΅) |
22 | 21 | sseq2d 3975 |
. . . . . . . . . . 11
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β ({π₯, π¦} β (Baseβπ) β {π₯, π¦} β π΅)) |
23 | | ovex 7383 |
. . . . . . . . . . . . . . 15
β’
(β0 βm π) β V |
24 | 23 | rabex 5288 |
. . . . . . . . . . . . . 14
β’ {β β (β0
βm π)
β£ (β‘β β β) β Fin} β
V |
25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β {β β (β0
βm π)
β£ (β‘β β β) β Fin} β
V) |
26 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β π = πΌ) |
27 | 26 | oveq2d 7366 |
. . . . . . . . . . . . . . 15
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β (β0
βm π) =
(β0 βm πΌ)) |
28 | | rabeq 3420 |
. . . . . . . . . . . . . . 15
β’
((β0 βm π) = (β0 βm
πΌ) β {β β (β0
βm π)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β {β β (β0
βm π)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin}) |
30 | | opsrval.d |
. . . . . . . . . . . . . 14
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
31 | 29, 30 | eqtr4di 2796 |
. . . . . . . . . . . . 13
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β {β β (β0
βm π)
β£ (β‘β β β) β Fin} = π·) |
32 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β π = π·) |
33 | | simpllr 775 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β π = π
) |
34 | 33 | fveq2d 6842 |
. . . . . . . . . . . . . . . . 17
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (ltβπ ) = (ltβπ
)) |
35 | | opsrval.q |
. . . . . . . . . . . . . . . . 17
β’ < =
(ltβπ
) |
36 | 34, 35 | eqtr4di 2796 |
. . . . . . . . . . . . . . . 16
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (ltβπ ) = < ) |
37 | 36 | breqd 5115 |
. . . . . . . . . . . . . . 15
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β ((π₯βπ§)(ltβπ )(π¦βπ§) β (π₯βπ§) < (π¦βπ§))) |
38 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β π = πΌ) |
39 | 38 | oveq2d 7366 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (π <bag π) = (π <bag πΌ)) |
40 | 39 | breqd 5115 |
. . . . . . . . . . . . . . . . 17
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (π€(π <bag π)π§ β π€(π <bag πΌ)π§)) |
41 | 40 | imbi1d 342 |
. . . . . . . . . . . . . . . 16
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β ((π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€)) β (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€)))) |
42 | 32, 41 | raleqbidv 3318 |
. . . . . . . . . . . . . . 15
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€)) β βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€)))) |
43 | 37, 42 | anbi12d 632 |
. . . . . . . . . . . . . 14
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))))) |
44 | 32, 43 | rexeqbidv 3319 |
. . . . . . . . . . . . 13
β’ ((((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β§ π = π·) β (βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))))) |
45 | 25, 31, 44 | sbcied2 3785 |
. . . . . . . . . . . 12
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))))) |
46 | 45 | orbi1d 916 |
. . . . . . . . . . 11
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β (([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦) β (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))) |
47 | 22, 46 | anbi12d 632 |
. . . . . . . . . 10
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β (({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦)) β ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦)))) |
48 | 47 | opabbidv 5170 |
. . . . . . . . 9
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}) |
49 | 48 | opeq2d 4836 |
. . . . . . . 8
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β© = β¨(leβndx),
{β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©) |
50 | 18, 49 | oveq12d 7368 |
. . . . . . 7
β’ (((π = πΌ β§ π = π
) β§ π = (π mPwSer π )) β (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©) = (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) |
51 | 13, 50 | csbied 3892 |
. . . . . 6
β’ ((π = πΌ β§ π = π
) β β¦(π mPwSer π ) / πβ¦(π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©) = (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) |
52 | 12, 51 | mpteq12dv 5195 |
. . . . 5
β’ ((π = πΌ β§ π = π
) β (π β π« (π Γ π) β¦ β¦(π mPwSer π ) / πβ¦(π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) = (π β π« (πΌ Γ πΌ) β¦ (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©))) |
53 | | df-opsr 21239 |
. . . . 5
β’ ordPwSer
= (π β V, π β V β¦ (π β π« (π Γ π) β¦ β¦(π mPwSer π ) / πβ¦(π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β (Baseβπ) β§ ([{β β (β0
βm π)
β£ (β‘β β β) β Fin} / π]βπ§ β π ((π₯βπ§)(ltβπ )(π¦βπ§) β§ βπ€ β π (π€(π <bag π)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©))) |
54 | 52, 53 | ovmpoga 7502 |
. . . 4
β’ ((πΌ β V β§ π
β V β§ (π β π« (πΌ Γ πΌ) β¦ (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) β V) β (πΌ ordPwSer π
) = (π β π« (πΌ Γ πΌ) β¦ (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©))) |
55 | 3, 5, 9, 54 | syl3anc 1372 |
. . 3
β’ (π β (πΌ ordPwSer π
) = (π β π« (πΌ Γ πΌ) β¦ (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©))) |
56 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π = π) β π = π) |
57 | 56 | oveq1d 7365 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π = π) β (π <bag πΌ) = (π <bag πΌ)) |
58 | | opsrval.c |
. . . . . . . . . . . . . . 15
β’ πΆ = (π <bag πΌ) |
59 | 57, 58 | eqtr4di 2796 |
. . . . . . . . . . . . . 14
β’ ((π β§ π = π) β (π <bag πΌ) = πΆ) |
60 | 59 | breqd 5115 |
. . . . . . . . . . . . 13
β’ ((π β§ π = π) β (π€(π <bag πΌ)π§ β π€πΆπ§)) |
61 | 60 | imbi1d 342 |
. . . . . . . . . . . 12
β’ ((π β§ π = π) β ((π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€)) β (π€πΆπ§ β (π₯βπ€) = (π¦βπ€)))) |
62 | 61 | ralbidv 3173 |
. . . . . . . . . . 11
β’ ((π β§ π = π) β (βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€)) β βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€)))) |
63 | 62 | anbi2d 630 |
. . . . . . . . . 10
β’ ((π β§ π = π) β (((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))))) |
64 | 63 | rexbidv 3174 |
. . . . . . . . 9
β’ ((π β§ π = π) β (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))))) |
65 | 64 | orbi1d 916 |
. . . . . . . 8
β’ ((π β§ π = π) β ((βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦) β (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))) |
66 | 65 | anbi2d 630 |
. . . . . . 7
β’ ((π β§ π = π) β (({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦)) β ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦)))) |
67 | 66 | opabbidv 5170 |
. . . . . 6
β’ ((π β§ π = π) β {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}) |
68 | | opsrval.l |
. . . . . 6
β’ β€ =
{β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} |
69 | 67, 68 | eqtr4di 2796 |
. . . . 5
β’ ((π β§ π = π) β {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = β€ ) |
70 | 69 | opeq2d 4836 |
. . . 4
β’ ((π β§ π = π) β β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β© = β¨(leβndx), β€
β©) |
71 | 70 | oveq2d 7366 |
. . 3
β’ ((π β§ π = π) β (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€(π <bag πΌ)π§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©) = (π sSet β¨(leβndx), β€
β©)) |
72 | | opsrval.t |
. . . 4
β’ (π β π β (πΌ Γ πΌ)) |
73 | 6, 72 | sselpwd 5282 |
. . 3
β’ (π β π β π« (πΌ Γ πΌ)) |
74 | | ovexd 7385 |
. . 3
β’ (π β (π sSet β¨(leβndx), β€ β©)
β V) |
75 | 55, 71, 73, 74 | fvmptd 6951 |
. 2
β’ (π β ((πΌ ordPwSer π
)βπ) = (π sSet β¨(leβndx), β€
β©)) |
76 | 1, 75 | eqtrid 2790 |
1
β’ (π β π = (π sSet β¨(leβndx), β€
β©)) |