Step | Hyp | Ref
| Expression |
1 | | simpr1 1195 |
. . . . . . . 8
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΉ β π·) |
2 | | psrbag.d |
. . . . . . . . . 10
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
3 | 2 | psrbag 21335 |
. . . . . . . . 9
β’ (πΌ β π β (πΉ β π· β (πΉ:πΌβΆβ0 β§ (β‘πΉ β β) β
Fin))) |
4 | 3 | adantr 482 |
. . . . . . . 8
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ β π· β (πΉ:πΌβΆβ0 β§ (β‘πΉ β β) β
Fin))) |
5 | 1, 4 | mpbid 231 |
. . . . . . 7
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ:πΌβΆβ0 β§ (β‘πΉ β β) β
Fin)) |
6 | 5 | simpld 496 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΉ:πΌβΆβ0) |
7 | 6 | ffnd 6670 |
. . . . 5
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΉ Fn πΌ) |
8 | | simpr2 1196 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ:πΌβΆβ0) |
9 | 8 | ffnd 6670 |
. . . . 5
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ Fn πΌ) |
10 | | simpl 484 |
. . . . 5
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΌ β π) |
11 | | inidm 4179 |
. . . . 5
β’ (πΌ β© πΌ) = πΌ |
12 | 7, 9, 10, 10, 11 | offn 7631 |
. . . 4
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ βf β πΊ) Fn πΌ) |
13 | | eqidd 2734 |
. . . . . . 7
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΉβπ₯) = (πΉβπ₯)) |
14 | | eqidd 2734 |
. . . . . . 7
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΊβπ₯) = (πΊβπ₯)) |
15 | 7, 9, 10, 10, 11, 13, 14 | ofval 7629 |
. . . . . 6
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β ((πΉ βf β πΊ)βπ₯) = ((πΉβπ₯) β (πΊβπ₯))) |
16 | | simpr3 1197 |
. . . . . . . . 9
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β πΊ βr β€ πΉ) |
17 | 9, 7, 10, 10, 11, 14, 13 | ofrfval 7628 |
. . . . . . . . 9
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΊ βr β€ πΉ β βπ₯ β πΌ (πΊβπ₯) β€ (πΉβπ₯))) |
18 | 16, 17 | mpbid 231 |
. . . . . . . 8
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β βπ₯ β πΌ (πΊβπ₯) β€ (πΉβπ₯)) |
19 | 18 | r19.21bi 3233 |
. . . . . . 7
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΊβπ₯) β€ (πΉβπ₯)) |
20 | 8 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΊβπ₯) β
β0) |
21 | 6 | ffvelcdmda 7036 |
. . . . . . . 8
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (πΉβπ₯) β
β0) |
22 | | nn0sub 12468 |
. . . . . . . 8
β’ (((πΊβπ₯) β β0 β§ (πΉβπ₯) β β0) β ((πΊβπ₯) β€ (πΉβπ₯) β ((πΉβπ₯) β (πΊβπ₯)) β
β0)) |
23 | 20, 21, 22 | syl2anc 585 |
. . . . . . 7
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β ((πΊβπ₯) β€ (πΉβπ₯) β ((πΉβπ₯) β (πΊβπ₯)) β
β0)) |
24 | 19, 23 | mpbid 231 |
. . . . . 6
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β ((πΉβπ₯) β (πΊβπ₯)) β
β0) |
25 | 15, 24 | eqeltrd 2834 |
. . . . 5
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β ((πΉ βf β πΊ)βπ₯) β
β0) |
26 | 25 | ralrimiva 3140 |
. . . 4
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β βπ₯ β πΌ ((πΉ βf β πΊ)βπ₯) β
β0) |
27 | | ffnfv 7067 |
. . . 4
β’ ((πΉ βf β
πΊ):πΌβΆβ0 β ((πΉ βf β
πΊ) Fn πΌ β§ βπ₯ β πΌ ((πΉ βf β πΊ)βπ₯) β
β0)) |
28 | 12, 26, 27 | sylanbrc 584 |
. . 3
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ βf β πΊ):πΌβΆβ0) |
29 | 5 | simprd 497 |
. . . 4
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (β‘πΉ β β) β
Fin) |
30 | 20 | nn0ge0d 12481 |
. . . . . . . 8
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β 0 β€ (πΊβπ₯)) |
31 | | nn0re 12427 |
. . . . . . . . . 10
β’ ((πΉβπ₯) β β0 β (πΉβπ₯) β β) |
32 | | nn0re 12427 |
. . . . . . . . . 10
β’ ((πΊβπ₯) β β0 β (πΊβπ₯) β β) |
33 | | subge02 11676 |
. . . . . . . . . 10
β’ (((πΉβπ₯) β β β§ (πΊβπ₯) β β) β (0 β€ (πΊβπ₯) β ((πΉβπ₯) β (πΊβπ₯)) β€ (πΉβπ₯))) |
34 | 31, 32, 33 | syl2an 597 |
. . . . . . . . 9
β’ (((πΉβπ₯) β β0 β§ (πΊβπ₯) β β0) β (0 β€
(πΊβπ₯) β ((πΉβπ₯) β (πΊβπ₯)) β€ (πΉβπ₯))) |
35 | 21, 20, 34 | syl2anc 585 |
. . . . . . . 8
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β (0 β€ (πΊβπ₯) β ((πΉβπ₯) β (πΊβπ₯)) β€ (πΉβπ₯))) |
36 | 30, 35 | mpbid 231 |
. . . . . . 7
β’ (((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β§ π₯ β πΌ) β ((πΉβπ₯) β (πΊβπ₯)) β€ (πΉβπ₯)) |
37 | 36 | ralrimiva 3140 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β βπ₯ β πΌ ((πΉβπ₯) β (πΊβπ₯)) β€ (πΉβπ₯)) |
38 | 12, 7, 10, 10, 11, 15, 13 | ofrfval 7628 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β ((πΉ βf β πΊ) βr β€ πΉ β βπ₯ β πΌ ((πΉβπ₯) β (πΊβπ₯)) β€ (πΉβπ₯))) |
39 | 37, 38 | mpbird 257 |
. . . . 5
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ βf β πΊ) βr β€ πΉ) |
40 | 2 | psrbaglesuppOLD 21343 |
. . . . 5
β’ ((πΌ β π β§ (πΉ β π· β§ (πΉ βf β πΊ):πΌβΆβ0 β§ (πΉ βf β
πΊ) βr β€
πΉ)) β (β‘(πΉ βf β πΊ) β β) β
(β‘πΉ β β)) |
41 | 10, 1, 28, 39, 40 | syl13anc 1373 |
. . . 4
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (β‘(πΉ βf β πΊ) β β) β
(β‘πΉ β β)) |
42 | 29, 41 | ssfid 9214 |
. . 3
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (β‘(πΉ βf β πΊ) β β) β
Fin) |
43 | 2 | psrbag 21335 |
. . . 4
β’ (πΌ β π β ((πΉ βf β πΊ) β π· β ((πΉ βf β πΊ):πΌβΆβ0 β§ (β‘(πΉ βf β πΊ) β β) β
Fin))) |
44 | 43 | adantr 482 |
. . 3
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β ((πΉ βf β πΊ) β π· β ((πΉ βf β πΊ):πΌβΆβ0 β§ (β‘(πΉ βf β πΊ) β β) β
Fin))) |
45 | 28, 42, 44 | mpbir2and 712 |
. 2
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β (πΉ βf β πΊ) β π·) |
46 | 45, 39 | jca 513 |
1
β’ ((πΌ β π β§ (πΉ β π· β§ πΊ:πΌβΆβ0 β§ πΊ βr β€ πΉ)) β ((πΉ βf β πΊ) β π· β§ (πΉ βf β πΊ) βr β€ πΉ)) |