Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’ (π₯ β π β¦ (πΉ βf β π₯)) = (π₯ β π β¦ (πΉ βf β π₯)) |
2 | | simpll 766 |
. . . 4
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β πΌ β π) |
3 | | simplr 768 |
. . . 4
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β πΉ β π·) |
4 | | simpr 486 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β π₯ β π) |
5 | | breq1 5109 |
. . . . . . . 8
β’ (π¦ = π₯ β (π¦ βr β€ πΉ β π₯ βr β€ πΉ)) |
6 | | psrbagconf1o.s |
. . . . . . . 8
β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} |
7 | 5, 6 | elrab2 3649 |
. . . . . . 7
β’ (π₯ β π β (π₯ β π· β§ π₯ βr β€ πΉ)) |
8 | 4, 7 | sylib 217 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β (π₯ β π· β§ π₯ βr β€ πΉ)) |
9 | 8 | simpld 496 |
. . . . 5
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β π₯ β π·) |
10 | | psrbag.d |
. . . . . 6
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
11 | 10 | psrbagfOLD 21337 |
. . . . 5
β’ ((πΌ β π β§ π₯ β π·) β π₯:πΌβΆβ0) |
12 | 2, 9, 11 | syl2anc 585 |
. . . 4
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β π₯:πΌβΆβ0) |
13 | 8 | simprd 497 |
. . . 4
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β π₯ βr β€ πΉ) |
14 | 10 | psrbagconOLD 21349 |
. . . 4
β’ ((πΌ β π β§ (πΉ β π· β§ π₯:πΌβΆβ0 β§ π₯ βr β€ πΉ)) β ((πΉ βf β π₯) β π· β§ (πΉ βf β π₯) βr β€ πΉ)) |
15 | 2, 3, 12, 13, 14 | syl13anc 1373 |
. . 3
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β ((πΉ βf β π₯) β π· β§ (πΉ βf β π₯) βr β€ πΉ)) |
16 | | breq1 5109 |
. . . 4
β’ (π¦ = (πΉ βf β π₯) β (π¦ βr β€ πΉ β (πΉ βf β π₯) βr β€ πΉ)) |
17 | 16, 6 | elrab2 3649 |
. . 3
β’ ((πΉ βf β
π₯) β π β ((πΉ βf β π₯) β π· β§ (πΉ βf β π₯) βr β€ πΉ)) |
18 | 15, 17 | sylibr 233 |
. 2
β’ (((πΌ β π β§ πΉ β π·) β§ π₯ β π) β (πΉ βf β π₯) β π) |
19 | 18 | ralrimiva 3140 |
. . 3
β’ ((πΌ β π β§ πΉ β π·) β βπ₯ β π (πΉ βf β π₯) β π) |
20 | | oveq2 7366 |
. . . . 5
β’ (π₯ = π§ β (πΉ βf β π₯) = (πΉ βf β π§)) |
21 | 20 | eleq1d 2819 |
. . . 4
β’ (π₯ = π§ β ((πΉ βf β π₯) β π β (πΉ βf β π§) β π)) |
22 | 21 | rspccva 3579 |
. . 3
β’
((βπ₯ β
π (πΉ βf β π₯) β π β§ π§ β π) β (πΉ βf β π§) β π) |
23 | 19, 22 | sylan 581 |
. 2
β’ (((πΌ β π β§ πΉ β π·) β§ π§ β π) β (πΉ βf β π§) β π) |
24 | 10 | psrbagfOLD 21337 |
. . . . . . . . 9
β’ ((πΌ β π β§ πΉ β π·) β πΉ:πΌβΆβ0) |
25 | 24 | adantr 482 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β πΉ:πΌβΆβ0) |
26 | 25 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (πΉβπ) β
β0) |
27 | | simpll 766 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β πΌ β π) |
28 | 6 | ssrab3 4041 |
. . . . . . . . . 10
β’ π β π· |
29 | | simprr 772 |
. . . . . . . . . 10
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β π§ β π) |
30 | 28, 29 | sselid 3943 |
. . . . . . . . 9
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β π§ β π·) |
31 | 10 | psrbagfOLD 21337 |
. . . . . . . . 9
β’ ((πΌ β π β§ π§ β π·) β π§:πΌβΆβ0) |
32 | 27, 30, 31 | syl2anc 585 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β π§:πΌβΆβ0) |
33 | 32 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π§βπ) β
β0) |
34 | 12 | adantrr 716 |
. . . . . . . 8
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β π₯:πΌβΆβ0) |
35 | 34 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π₯βπ) β
β0) |
36 | | nn0cn 12428 |
. . . . . . . 8
β’ ((πΉβπ) β β0 β (πΉβπ) β β) |
37 | | nn0cn 12428 |
. . . . . . . 8
β’ ((π§βπ) β β0 β (π§βπ) β β) |
38 | | nn0cn 12428 |
. . . . . . . 8
β’ ((π₯βπ) β β0 β (π₯βπ) β β) |
39 | | subsub23 11411 |
. . . . . . . 8
β’ (((πΉβπ) β β β§ (π§βπ) β β β§ (π₯βπ) β β) β (((πΉβπ) β (π§βπ)) = (π₯βπ) β ((πΉβπ) β (π₯βπ)) = (π§βπ))) |
40 | 36, 37, 38, 39 | syl3an 1161 |
. . . . . . 7
β’ (((πΉβπ) β β0 β§ (π§βπ) β β0 β§ (π₯βπ) β β0) β (((πΉβπ) β (π§βπ)) = (π₯βπ) β ((πΉβπ) β (π₯βπ)) = (π§βπ))) |
41 | 26, 33, 35, 40 | syl3anc 1372 |
. . . . . 6
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (((πΉβπ) β (π§βπ)) = (π₯βπ) β ((πΉβπ) β (π₯βπ)) = (π§βπ))) |
42 | | eqcom 2740 |
. . . . . 6
β’ ((π₯βπ) = ((πΉβπ) β (π§βπ)) β ((πΉβπ) β (π§βπ)) = (π₯βπ)) |
43 | | eqcom 2740 |
. . . . . 6
β’ ((π§βπ) = ((πΉβπ) β (π₯βπ)) β ((πΉβπ) β (π₯βπ)) = (π§βπ)) |
44 | 41, 42, 43 | 3bitr4g 314 |
. . . . 5
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π₯βπ) = ((πΉβπ) β (π§βπ)) β (π§βπ) = ((πΉβπ) β (π₯βπ)))) |
45 | 25 | ffnd 6670 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β πΉ Fn πΌ) |
46 | 32 | ffnd 6670 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β π§ Fn πΌ) |
47 | | inidm 4179 |
. . . . . . 7
β’ (πΌ β© πΌ) = πΌ |
48 | | eqidd 2734 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (πΉβπ) = (πΉβπ)) |
49 | | eqidd 2734 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π§βπ) = (π§βπ)) |
50 | 45, 46, 27, 27, 47, 48, 49 | ofval 7629 |
. . . . . 6
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((πΉ βf β π§)βπ) = ((πΉβπ) β (π§βπ))) |
51 | 50 | eqeq2d 2744 |
. . . . 5
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π₯βπ) = ((πΉ βf β π§)βπ) β (π₯βπ) = ((πΉβπ) β (π§βπ)))) |
52 | 34 | ffnd 6670 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β π₯ Fn πΌ) |
53 | | eqidd 2734 |
. . . . . . 7
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π₯βπ) = (π₯βπ)) |
54 | 45, 52, 27, 27, 47, 48, 53 | ofval 7629 |
. . . . . 6
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((πΉ βf β π₯)βπ) = ((πΉβπ) β (π₯βπ))) |
55 | 54 | eqeq2d 2744 |
. . . . 5
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π§βπ) = ((πΉ βf β π₯)βπ) β (π§βπ) = ((πΉβπ) β (π₯βπ)))) |
56 | 44, 51, 55 | 3bitr4d 311 |
. . . 4
β’ ((((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π₯βπ) = ((πΉ βf β π§)βπ) β (π§βπ) = ((πΉ βf β π₯)βπ))) |
57 | 56 | ralbidva 3169 |
. . 3
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (βπ β πΌ (π₯βπ) = ((πΉ βf β π§)βπ) β βπ β πΌ (π§βπ) = ((πΉ βf β π₯)βπ))) |
58 | 23 | adantrl 715 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§) β π) |
59 | 28, 58 | sselid 3943 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§) β π·) |
60 | 10 | psrbagfOLD 21337 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ βf β π§) β π·) β (πΉ βf β π§):πΌβΆβ0) |
61 | 27, 59, 60 | syl2anc 585 |
. . . . 5
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§):πΌβΆβ0) |
62 | 61 | ffnd 6670 |
. . . 4
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§) Fn πΌ) |
63 | | eqfnfv 6983 |
. . . 4
β’ ((π₯ Fn πΌ β§ (πΉ βf β π§) Fn πΌ) β (π₯ = (πΉ βf β π§) β βπ β πΌ (π₯βπ) = ((πΉ βf β π§)βπ))) |
64 | 52, 62, 63 | syl2anc 585 |
. . 3
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (π₯ = (πΉ βf β π§) β βπ β πΌ (π₯βπ) = ((πΉ βf β π§)βπ))) |
65 | 18 | adantrr 716 |
. . . . . . 7
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π₯) β π) |
66 | 28, 65 | sselid 3943 |
. . . . . 6
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π₯) β π·) |
67 | 10 | psrbagfOLD 21337 |
. . . . . 6
β’ ((πΌ β π β§ (πΉ βf β π₯) β π·) β (πΉ βf β π₯):πΌβΆβ0) |
68 | 27, 66, 67 | syl2anc 585 |
. . . . 5
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π₯):πΌβΆβ0) |
69 | 68 | ffnd 6670 |
. . . 4
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π₯) Fn πΌ) |
70 | | eqfnfv 6983 |
. . . 4
β’ ((π§ Fn πΌ β§ (πΉ βf β π₯) Fn πΌ) β (π§ = (πΉ βf β π₯) β βπ β πΌ (π§βπ) = ((πΉ βf β π₯)βπ))) |
71 | 46, 69, 70 | syl2anc 585 |
. . 3
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (π§ = (πΉ βf β π₯) β βπ β πΌ (π§βπ) = ((πΉ βf β π₯)βπ))) |
72 | 57, 64, 71 | 3bitr4d 311 |
. 2
β’ (((πΌ β π β§ πΉ β π·) β§ (π₯ β π β§ π§ β π)) β (π₯ = (πΉ βf β π§) β π§ = (πΉ βf β π₯))) |
73 | 1, 18, 23, 72 | f1o2d 7608 |
1
β’ ((πΌ β π β§ πΉ β π·) β (π₯ β π β¦ (πΉ βf β π₯)):πβ1-1-ontoβπ) |