Step | Hyp | Ref
| Expression |
1 | | opsrle.s |
. . . . 5
β’ π = (πΌ mPwSer π
) |
2 | | opsrle.o |
. . . . 5
β’ π = ((πΌ ordPwSer π
)βπ) |
3 | | opsrle.b |
. . . . 5
β’ π΅ = (Baseβπ) |
4 | | opsrle.q |
. . . . 5
β’ < =
(ltβπ
) |
5 | | opsrle.c |
. . . . 5
β’ πΆ = (π <bag πΌ) |
6 | | opsrle.d |
. . . . 5
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
7 | | eqid 2733 |
. . . . 5
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} |
8 | | simprl 770 |
. . . . 5
β’ ((π β§ (πΌ β V β§ π
β V)) β πΌ β V) |
9 | | simprr 772 |
. . . . 5
β’ ((π β§ (πΌ β V β§ π
β V)) β π
β V) |
10 | | opsrle.t |
. . . . . 6
β’ (π β π β (πΌ Γ πΌ)) |
11 | 10 | adantr 482 |
. . . . 5
β’ ((π β§ (πΌ β V β§ π
β V)) β π β (πΌ Γ πΌ)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 11 | opsrval 21463 |
. . . 4
β’ ((π β§ (πΌ β V β§ π
β V)) β π = (π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) |
13 | 12 | fveq2d 6847 |
. . 3
β’ ((π β§ (πΌ β V β§ π
β V)) β (leβπ) = (leβ(π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©))) |
14 | | opsrle.l |
. . 3
β’ β€ =
(leβπ) |
15 | 1 | ovexi 7392 |
. . . 4
β’ π β V |
16 | 3 | fvexi 6857 |
. . . . . 6
β’ π΅ β V |
17 | 16, 16 | xpex 7688 |
. . . . 5
β’ (π΅ Γ π΅) β V |
18 | | vex 3448 |
. . . . . . . . 9
β’ π₯ β V |
19 | | vex 3448 |
. . . . . . . . 9
β’ π¦ β V |
20 | 18, 19 | prss 4781 |
. . . . . . . 8
β’ ((π₯ β π΅ β§ π¦ β π΅) β {π₯, π¦} β π΅) |
21 | 20 | anbi1i 625 |
. . . . . . 7
β’ (((π₯ β π΅ β§ π¦ β π΅) β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦)) β ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))) |
22 | 21 | opabbii 5173 |
. . . . . 6
β’
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} |
23 | | opabssxp 5725 |
. . . . . 6
β’
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} β (π΅ Γ π΅) |
24 | 22, 23 | eqsstrri 3980 |
. . . . 5
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} β (π΅ Γ π΅) |
25 | 17, 24 | ssexi 5280 |
. . . 4
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} β V |
26 | | pleid 17253 |
. . . . 5
β’ le = Slot
(leβndx) |
27 | 26 | setsid 17085 |
. . . 4
β’ ((π β V β§ {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} β V) β {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = (leβ(π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©))) |
28 | 15, 25, 27 | mp2an 691 |
. . 3
β’
{β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = (leβ(π sSet β¨(leβndx), {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}β©)) |
29 | 13, 14, 28 | 3eqtr4g 2798 |
. 2
β’ ((π β§ (πΌ β V β§ π
β V)) β β€ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}) |
30 | | reldmopsr 21462 |
. . . . . . . . . 10
β’ Rel dom
ordPwSer |
31 | 30 | ovprc 7396 |
. . . . . . . . 9
β’ (Β¬
(πΌ β V β§ π
β V) β (πΌ ordPwSer π
) = β
) |
32 | 31 | adantl 483 |
. . . . . . . 8
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β (πΌ ordPwSer π
) = β
) |
33 | 32 | fveq1d 6845 |
. . . . . . 7
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β ((πΌ ordPwSer π
)βπ) = (β
βπ)) |
34 | 2, 33 | eqtrid 2785 |
. . . . . 6
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β π = (β
βπ)) |
35 | | 0fv 6887 |
. . . . . 6
β’
(β
βπ) =
β
|
36 | 34, 35 | eqtrdi 2789 |
. . . . 5
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β π = β
) |
37 | 36 | fveq2d 6847 |
. . . 4
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β (leβπ) =
(leββ
)) |
38 | 26 | str0 17066 |
. . . 4
β’ β
=
(leββ
) |
39 | 37, 14, 38 | 3eqtr4g 2798 |
. . 3
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β β€ =
β
) |
40 | | reldmpsr 21332 |
. . . . . . . . . . 11
β’ Rel dom
mPwSer |
41 | 40 | ovprc 7396 |
. . . . . . . . . 10
β’ (Β¬
(πΌ β V β§ π
β V) β (πΌ mPwSer π
) = β
) |
42 | 41 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β (πΌ mPwSer π
) = β
) |
43 | 1, 42 | eqtrid 2785 |
. . . . . . . 8
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β π = β
) |
44 | 43 | fveq2d 6847 |
. . . . . . 7
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β (Baseβπ) =
(Baseββ
)) |
45 | | base0 17093 |
. . . . . . 7
β’ β
=
(Baseββ
) |
46 | 44, 3, 45 | 3eqtr4g 2798 |
. . . . . 6
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β π΅ = β
) |
47 | 46 | xpeq2d 5664 |
. . . . 5
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β (π΅ Γ π΅) = (π΅ Γ β
)) |
48 | | xp0 6111 |
. . . . 5
β’ (π΅ Γ β
) =
β
|
49 | 47, 48 | eqtrdi 2789 |
. . . 4
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β (π΅ Γ π΅) = β
) |
50 | | sseq0 4360 |
. . . 4
β’
(({β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} β (π΅ Γ π΅) β§ (π΅ Γ π΅) = β
) β {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = β
) |
51 | 24, 49, 50 | sylancr 588 |
. . 3
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))} = β
) |
52 | 39, 51 | eqtr4d 2776 |
. 2
β’ ((π β§ Β¬ (πΌ β V β§ π
β V)) β β€ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}) |
53 | 29, 52 | pm2.61dan 812 |
1
β’ (π β β€ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ (βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€))) β¨ π₯ = π¦))}) |