Step | Hyp | Ref
| Expression |
1 | | simprr 770 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
2 | | breq1 5151 |
. . . . . 6
β’ (π₯ = π β (π₯ βr β€ (πΉ βf β π) β π βr β€ (πΉ βf β π))) |
3 | 2 | elrab 3683 |
. . . . 5
β’ (π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)} β (π β π· β§ π βr β€ (πΉ βf β π))) |
4 | 1, 3 | sylib 217 |
. . . 4
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π· β§ π βr β€ (πΉ βf β π))) |
5 | 4 | simpld 494 |
. . 3
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π·) |
6 | 4 | simprd 495 |
. . . 4
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π βr β€ (πΉ βf β π)) |
7 | | gsumbagdiagOLD.i |
. . . . . . 7
β’ (π β πΌ β π) |
8 | 7 | adantr 480 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β πΌ β π) |
9 | | gsumbagdiagOLD.f |
. . . . . . 7
β’ (π β πΉ β π·) |
10 | 9 | adantr 480 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β πΉ β π·) |
11 | | simprl 768 |
. . . . . . . . 9
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π) |
12 | | breq1 5151 |
. . . . . . . . . 10
β’ (π¦ = π β (π¦ βr β€ πΉ β π βr β€ πΉ)) |
13 | | psrbagconf1o.s |
. . . . . . . . . 10
β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} |
14 | 12, 13 | elrab2 3686 |
. . . . . . . . 9
β’ (π β π β (π β π· β§ π βr β€ πΉ)) |
15 | 11, 14 | sylib 217 |
. . . . . . . 8
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π· β§ π βr β€ πΉ)) |
16 | 15 | simpld 494 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π·) |
17 | | psrbag.d |
. . . . . . . 8
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
18 | 17 | psrbagfOLD 21692 |
. . . . . . 7
β’ ((πΌ β π β§ π β π·) β π:πΌβΆβ0) |
19 | 8, 16, 18 | syl2anc 583 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π:πΌβΆβ0) |
20 | 15 | simprd 495 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π βr β€ πΉ) |
21 | 17 | psrbagconOLD 21704 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ π:πΌβΆβ0 β§ π βr β€ πΉ)) β ((πΉ βf β π) β π· β§ (πΉ βf β π) βr β€ πΉ)) |
22 | 8, 10, 19, 20, 21 | syl13anc 1371 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β ((πΉ βf β π) β π· β§ (πΉ βf β π) βr β€ πΉ)) |
23 | 22 | simprd 495 |
. . . 4
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (πΉ βf β π) βr β€ πΉ) |
24 | 17 | psrbagfOLD 21692 |
. . . . . 6
β’ ((πΌ β π β§ π β π·) β π:πΌβΆβ0) |
25 | 8, 5, 24 | syl2anc 583 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π:πΌβΆβ0) |
26 | 22 | simpld 494 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (πΉ βf β π) β π·) |
27 | 17 | psrbagfOLD 21692 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ βf β π) β π·) β (πΉ βf β π):πΌβΆβ0) |
28 | 8, 26, 27 | syl2anc 583 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (πΉ βf β π):πΌβΆβ0) |
29 | 17 | psrbagfOLD 21692 |
. . . . . 6
β’ ((πΌ β π β§ πΉ β π·) β πΉ:πΌβΆβ0) |
30 | 8, 10, 29 | syl2anc 583 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β πΉ:πΌβΆβ0) |
31 | | nn0re 12486 |
. . . . . . 7
β’ (π’ β β0
β π’ β
β) |
32 | | nn0re 12486 |
. . . . . . 7
β’ (π£ β β0
β π£ β
β) |
33 | | nn0re 12486 |
. . . . . . 7
β’ (π€ β β0
β π€ β
β) |
34 | | letr 11313 |
. . . . . . 7
β’ ((π’ β β β§ π£ β β β§ π€ β β) β ((π’ β€ π£ β§ π£ β€ π€) β π’ β€ π€)) |
35 | 31, 32, 33, 34 | syl3an 1159 |
. . . . . 6
β’ ((π’ β β0
β§ π£ β
β0 β§ π€
β β0) β ((π’ β€ π£ β§ π£ β€ π€) β π’ β€ π€)) |
36 | 35 | adantl 481 |
. . . . 5
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ (π’ β β0 β§ π£ β β0
β§ π€ β
β0)) β ((π’ β€ π£ β§ π£ β€ π€) β π’ β€ π€)) |
37 | 8, 25, 28, 30, 36 | caoftrn 7712 |
. . . 4
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β ((π βr β€ (πΉ βf β π) β§ (πΉ βf β π) βr β€ πΉ) β π βr β€ πΉ)) |
38 | 6, 23, 37 | mp2and 696 |
. . 3
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π βr β€ πΉ) |
39 | | breq1 5151 |
. . . 4
β’ (π¦ = π β (π¦ βr β€ πΉ β π βr β€ πΉ)) |
40 | 39, 13 | elrab2 3686 |
. . 3
β’ (π β π β (π β π· β§ π βr β€ πΉ)) |
41 | 5, 38, 40 | sylanbrc 582 |
. 2
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β π) |
42 | | breq1 5151 |
. . 3
β’ (π₯ = π β (π₯ βr β€ (πΉ βf β π) β π βr β€ (πΉ βf β π))) |
43 | 19 | ffvelcdmda 7086 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β (πβπ§) β
β0) |
44 | 25 | ffvelcdmda 7086 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β (πβπ§) β
β0) |
45 | 30 | ffvelcdmda 7086 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β (πΉβπ§) β
β0) |
46 | | nn0re 12486 |
. . . . . . . 8
β’ ((πβπ§) β β0 β (πβπ§) β β) |
47 | | nn0re 12486 |
. . . . . . . 8
β’ ((πβπ§) β β0 β (πβπ§) β β) |
48 | | nn0re 12486 |
. . . . . . . 8
β’ ((πΉβπ§) β β0 β (πΉβπ§) β β) |
49 | | leaddsub2 11696 |
. . . . . . . . 9
β’ (((πβπ§) β β β§ (πβπ§) β β β§ (πΉβπ§) β β) β (((πβπ§) + (πβπ§)) β€ (πΉβπ§) β (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
50 | | leaddsub 11695 |
. . . . . . . . 9
β’ (((πβπ§) β β β§ (πβπ§) β β β§ (πΉβπ§) β β) β (((πβπ§) + (πβπ§)) β€ (πΉβπ§) β (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
51 | 49, 50 | bitr3d 281 |
. . . . . . . 8
β’ (((πβπ§) β β β§ (πβπ§) β β β§ (πΉβπ§) β β) β ((πβπ§) β€ ((πΉβπ§) β (πβπ§)) β (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
52 | 46, 47, 48, 51 | syl3an 1159 |
. . . . . . 7
β’ (((πβπ§) β β0 β§ (πβπ§) β β0 β§ (πΉβπ§) β β0) β ((πβπ§) β€ ((πΉβπ§) β (πβπ§)) β (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
53 | 43, 44, 45, 52 | syl3anc 1370 |
. . . . . 6
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β ((πβπ§) β€ ((πΉβπ§) β (πβπ§)) β (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
54 | 53 | ralbidva 3174 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (βπ§ β πΌ (πβπ§) β€ ((πΉβπ§) β (πβπ§)) β βπ§ β πΌ (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
55 | | ovexd 7447 |
. . . . . 6
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β ((πΉβπ§) β (πβπ§)) β V) |
56 | 25 | feqmptd 6960 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π = (π§ β πΌ β¦ (πβπ§))) |
57 | 30 | ffnd 6718 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β πΉ Fn πΌ) |
58 | 19 | ffnd 6718 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π Fn πΌ) |
59 | | inidm 4218 |
. . . . . . 7
β’ (πΌ β© πΌ) = πΌ |
60 | | eqidd 2732 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β (πΉβπ§) = (πΉβπ§)) |
61 | | eqidd 2732 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β (πβπ§) = (πβπ§)) |
62 | 57, 58, 8, 8, 59, 60, 61 | offval 7683 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (πΉ βf β π) = (π§ β πΌ β¦ ((πΉβπ§) β (πβπ§)))) |
63 | 8, 44, 55, 56, 62 | ofrfval2 7695 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π βr β€ (πΉ βf β π) β βπ§ β πΌ (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
64 | | ovexd 7447 |
. . . . . 6
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β ((πΉβπ§) β (πβπ§)) β V) |
65 | 19 | feqmptd 6960 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π = (π§ β πΌ β¦ (πβπ§))) |
66 | 25 | ffnd 6718 |
. . . . . . 7
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π Fn πΌ) |
67 | | eqidd 2732 |
. . . . . . 7
β’ (((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β§ π§ β πΌ) β (πβπ§) = (πβπ§)) |
68 | 57, 66, 8, 8, 59, 60, 67 | offval 7683 |
. . . . . 6
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (πΉ βf β π) = (π§ β πΌ β¦ ((πΉβπ§) β (πβπ§)))) |
69 | 8, 43, 64, 65, 68 | ofrfval2 7695 |
. . . . 5
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π βr β€ (πΉ βf β π) β βπ§ β πΌ (πβπ§) β€ ((πΉβπ§) β (πβπ§)))) |
70 | 54, 63, 69 | 3bitr4d 311 |
. . . 4
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π βr β€ (πΉ βf β π) β π βr β€ (πΉ βf β π))) |
71 | 6, 70 | mpbid 231 |
. . 3
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π βr β€ (πΉ βf β π)) |
72 | 42, 16, 71 | elrabd 3685 |
. 2
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)}) |
73 | 41, 72 | jca 511 |
1
β’ ((π β§ (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) β (π β π β§ π β {π₯ β π· β£ π₯ βr β€ (πΉ βf β π)})) |