Step | Hyp | Ref
| Expression |
1 | | opsrtoslem.c |
. . . . . . . 8
β’ πΆ = (π <bag πΌ) |
2 | | opsrtoslem.d |
. . . . . . . 8
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
3 | | opsrso.i |
. . . . . . . 8
β’ (π β πΌ β π) |
4 | 3, 3 | xpexd 7689 |
. . . . . . . . 9
β’ (π β (πΌ Γ πΌ) β V) |
5 | | opsrso.t |
. . . . . . . . 9
β’ (π β π β (πΌ Γ πΌ)) |
6 | 4, 5 | ssexd 5285 |
. . . . . . . 8
β’ (π β π β V) |
7 | | opsrso.w |
. . . . . . . 8
β’ (π β π We πΌ) |
8 | 1, 2, 3, 6, 7 | ltbwe 21468 |
. . . . . . 7
β’ (π β πΆ We π·) |
9 | | opsrso.r |
. . . . . . . . 9
β’ (π β π
β Toset) |
10 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
11 | | eqid 2733 |
. . . . . . . . . . 11
β’
(leβπ
) =
(leβπ
) |
12 | | opsrtoslem.q |
. . . . . . . . . . 11
β’ < =
(ltβπ
) |
13 | 10, 11, 12 | tosso 18316 |
. . . . . . . . . 10
β’ (π
β Toset β (π
β Toset β ( < Or
(Baseβπ
) β§ ( I
βΎ (Baseβπ
))
β (leβπ
)))) |
14 | 13 | ibi 267 |
. . . . . . . . 9
β’ (π
β Toset β ( < Or
(Baseβπ
) β§ ( I
βΎ (Baseβπ
))
β (leβπ
))) |
15 | 9, 14 | syl 17 |
. . . . . . . 8
β’ (π β ( < Or (Baseβπ
) β§ ( I βΎ
(Baseβπ
)) β
(leβπ
))) |
16 | 15 | simpld 496 |
. . . . . . 7
β’ (π β < Or (Baseβπ
)) |
17 | | opsrtoslem.ps |
. . . . . . . . 9
β’ (π β βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€)))) |
18 | 17 | opabbii 5176 |
. . . . . . . 8
β’
{β¨π₯, π¦β© β£ π} = {β¨π₯, π¦β© β£ βπ§ β π· ((π₯βπ§) < (π¦βπ§) β§ βπ€ β π· (π€πΆπ§ β (π₯βπ€) = (π¦βπ€)))} |
19 | 18 | wemapso 9495 |
. . . . . . 7
β’ ((πΆ We π· β§ < Or (Baseβπ
)) β {β¨π₯, π¦β© β£ π} Or ((Baseβπ
) βm π·)) |
20 | 8, 16, 19 | syl2anc 585 |
. . . . . 6
β’ (π β {β¨π₯, π¦β© β£ π} Or ((Baseβπ
) βm π·)) |
21 | | opsrtoslem.s |
. . . . . . . 8
β’ π = (πΌ mPwSer π
) |
22 | | opsrtoslem.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
23 | 21, 10, 2, 22, 3 | psrbas 21369 |
. . . . . . 7
β’ (π β π΅ = ((Baseβπ
) βm π·)) |
24 | | soeq2 5571 |
. . . . . . 7
β’ (π΅ = ((Baseβπ
) βm π·) β ({β¨π₯, π¦β© β£ π} Or π΅ β {β¨π₯, π¦β© β£ π} Or ((Baseβπ
) βm π·))) |
25 | 23, 24 | syl 17 |
. . . . . 6
β’ (π β ({β¨π₯, π¦β© β£ π} Or π΅ β {β¨π₯, π¦β© β£ π} Or ((Baseβπ
) βm π·))) |
26 | 20, 25 | mpbird 257 |
. . . . 5
β’ (π β {β¨π₯, π¦β© β£ π} Or π΅) |
27 | | soinxp 5717 |
. . . . 5
β’
({β¨π₯, π¦β© β£ π} Or π΅ β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) Or π΅) |
28 | 26, 27 | sylib 217 |
. . . 4
β’ (π β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) Or π΅) |
29 | | opsrso.o |
. . . . . . . 8
β’ π = ((πΌ ordPwSer π
)βπ) |
30 | 29 | fvexi 6860 |
. . . . . . 7
β’ π β V |
31 | | opsrtoslem.l |
. . . . . . . 8
β’ β€ =
(leβπ) |
32 | | eqid 2733 |
. . . . . . . 8
β’
(ltβπ) =
(ltβπ) |
33 | 31, 32 | pltfval 18228 |
. . . . . . 7
β’ (π β V β (ltβπ) = ( β€ β I
)) |
34 | 30, 33 | ax-mp 5 |
. . . . . 6
β’
(ltβπ) = (
β€
β I ) |
35 | | difundir 4244 |
. . . . . . . 8
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅)) β I ) = ((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I ) βͺ (( I βΎ π΅) β I )) |
36 | | resss 5966 |
. . . . . . . . . 10
β’ ( I
βΎ π΅) β
I |
37 | | ssdif0 4327 |
. . . . . . . . . 10
β’ (( I
βΎ π΅) β I β
(( I βΎ π΅) β I )
= β
) |
38 | 36, 37 | mpbi 229 |
. . . . . . . . 9
β’ (( I
βΎ π΅) β I ) =
β
|
39 | 38 | uneq2i 4124 |
. . . . . . . 8
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I ) βͺ (( I βΎ π΅) β I )) = ((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I ) βͺ
β
) |
40 | | un0 4354 |
. . . . . . . 8
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I ) βͺ β
) =
(({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I ) |
41 | 35, 39, 40 | 3eqtri 2765 |
. . . . . . 7
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅)) β I ) = (({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I ) |
42 | 29, 3, 9, 5, 7, 21,
22, 12, 1, 2, 17, 31 | opsrtoslem1 21485 |
. . . . . . . 8
β’ (π β β€ = (({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅))) |
43 | 42 | difeq1d 4085 |
. . . . . . 7
β’ (π β ( β€ β I ) =
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅)) β I )) |
44 | | relinxp 5774 |
. . . . . . . . . . 11
β’ Rel
({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) |
45 | 44 | a1i 11 |
. . . . . . . . . 10
β’ (π β Rel ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))) |
46 | | df-br 5110 |
. . . . . . . . . . . . . 14
β’ (π I π β β¨π, πβ© β I ) |
47 | | vex 3451 |
. . . . . . . . . . . . . . 15
β’ π β V |
48 | 47 | ideq 5812 |
. . . . . . . . . . . . . 14
β’ (π I π β π = π) |
49 | 46, 48 | bitr3i 277 |
. . . . . . . . . . . . 13
β’
(β¨π, πβ© β I β π = π) |
50 | | brin 5161 |
. . . . . . . . . . . . . . . . . 18
β’ (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β (π{β¨π₯, π¦β© β£ π}π β§ π(π΅ Γ π΅)π)) |
51 | 50 | simprbi 498 |
. . . . . . . . . . . . . . . . 17
β’ (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β π(π΅ Γ π΅)π) |
52 | | brxp 5685 |
. . . . . . . . . . . . . . . . . 18
β’ (π(π΅ Γ π΅)π β (π β π΅ β§ π β π΅)) |
53 | 52 | simprbi 498 |
. . . . . . . . . . . . . . . . 17
β’ (π(π΅ Γ π΅)π β π β π΅) |
54 | 51, 53 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β π β π΅) |
55 | | sonr 5572 |
. . . . . . . . . . . . . . . . 17
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) Or π΅ β§ π β π΅) β Β¬ π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π) |
56 | 55 | ex 414 |
. . . . . . . . . . . . . . . 16
β’
(({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) Or π΅ β (π β π΅ β Β¬ π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π)) |
57 | 28, 54, 56 | syl2im 40 |
. . . . . . . . . . . . . . 15
β’ (π β (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β Β¬ π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π)) |
58 | 57 | pm2.01d 189 |
. . . . . . . . . . . . . 14
β’ (π β Β¬ π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π) |
59 | | breq2 5113 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π)) |
60 | | df-br 5110 |
. . . . . . . . . . . . . . . 16
β’ (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))) |
61 | 59, 60 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)))) |
62 | 61 | notbid 318 |
. . . . . . . . . . . . . 14
β’ (π = π β (Β¬ π({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))π β Β¬ β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)))) |
63 | 58, 62 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (π β (π = π β Β¬ β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)))) |
64 | 49, 63 | biimtrid 241 |
. . . . . . . . . . . 12
β’ (π β (β¨π, πβ© β I β Β¬ β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)))) |
65 | 64 | con2d 134 |
. . . . . . . . . . 11
β’ (π β (β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β Β¬ β¨π, πβ© β I )) |
66 | | opex 5425 |
. . . . . . . . . . . 12
β’
β¨π, πβ© β V |
67 | | eldif 3924 |
. . . . . . . . . . . 12
β’
(β¨π, πβ© β (V β I )
β (β¨π, πβ© β V β§ Β¬
β¨π, πβ© β I )) |
68 | 66, 67 | mpbiran 708 |
. . . . . . . . . . 11
β’
(β¨π, πβ© β (V β I )
β Β¬ β¨π, πβ© β I
) |
69 | 65, 68 | syl6ibr 252 |
. . . . . . . . . 10
β’ (π β (β¨π, πβ© β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β β¨π, πβ© β (V β I
))) |
70 | 45, 69 | relssdv 5748 |
. . . . . . . . 9
β’ (π β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β (V β I )) |
71 | | disj2 4421 |
. . . . . . . . 9
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β© I ) = β
β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β (V β I )) |
72 | 70, 71 | sylibr 233 |
. . . . . . . 8
β’ (π β (({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β© I ) = β
) |
73 | | disj3 4417 |
. . . . . . . 8
β’
((({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β© I ) = β
β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) = (({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I )) |
74 | 72, 73 | sylib 217 |
. . . . . . 7
β’ (π β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) = (({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β I )) |
75 | 41, 43, 74 | 3eqtr4a 2799 |
. . . . . 6
β’ (π β ( β€ β I ) =
({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))) |
76 | 34, 75 | eqtrid 2785 |
. . . . 5
β’ (π β (ltβπ) = ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅))) |
77 | | soeq1 5570 |
. . . . 5
β’
((ltβπ) =
({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) β ((ltβπ) Or π΅ β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) Or π΅)) |
78 | 76, 77 | syl 17 |
. . . 4
β’ (π β ((ltβπ) Or π΅ β ({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) Or π΅)) |
79 | 28, 78 | mpbird 257 |
. . 3
β’ (π β (ltβπ) Or π΅) |
80 | 21, 29, 5 | opsrbas 21475 |
. . . . 5
β’ (π β (Baseβπ) = (Baseβπ)) |
81 | 22, 80 | eqtrid 2785 |
. . . 4
β’ (π β π΅ = (Baseβπ)) |
82 | | soeq2 5571 |
. . . 4
β’ (π΅ = (Baseβπ) β ((ltβπ) Or π΅ β (ltβπ) Or (Baseβπ))) |
83 | 81, 82 | syl 17 |
. . 3
β’ (π β ((ltβπ) Or π΅ β (ltβπ) Or (Baseβπ))) |
84 | 79, 83 | mpbid 231 |
. 2
β’ (π β (ltβπ) Or (Baseβπ)) |
85 | 81 | reseq2d 5941 |
. . . 4
β’ (π β ( I βΎ π΅) = ( I βΎ
(Baseβπ))) |
86 | | ssun2 4137 |
. . . 4
β’ ( I
βΎ π΅) β
(({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅)) |
87 | 85, 86 | eqsstrrdi 4003 |
. . 3
β’ (π β ( I βΎ
(Baseβπ)) β
(({β¨π₯, π¦β© β£ π} β© (π΅ Γ π΅)) βͺ ( I βΎ π΅))) |
88 | 87, 42 | sseqtrrd 3989 |
. 2
β’ (π β ( I βΎ
(Baseβπ)) β
β€
) |
89 | | eqid 2733 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
90 | 89, 31, 32 | tosso 18316 |
. . 3
β’ (π β V β (π β Toset β
((ltβπ) Or
(Baseβπ) β§ ( I
βΎ (Baseβπ))
β β€ ))) |
91 | 30, 90 | ax-mp 5 |
. 2
β’ (π β Toset β
((ltβπ) Or
(Baseβπ) β§ ( I
βΎ (Baseβπ))
β β€ )) |
92 | 84, 88, 91 | sylanbrc 584 |
1
β’ (π β π β Toset) |