Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’ (π₯ β π β¦ (πΉ βf β π₯)) = (π₯ β π β¦ (πΉ βf β π₯)) |
2 | | psrbag.d |
. . 3
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
3 | | psrbagconf1o.s |
. . 3
β’ π = {π¦ β π· β£ π¦ βr β€ πΉ} |
4 | 2, 3 | psrbagconcl 21352 |
. 2
β’ ((πΉ β π· β§ π₯ β π) β (πΉ βf β π₯) β π) |
5 | 2, 3 | psrbagconcl 21352 |
. 2
β’ ((πΉ β π· β§ π§ β π) β (πΉ βf β π§) β π) |
6 | 2 | psrbagf 21336 |
. . . . . . . . 9
β’ (πΉ β π· β πΉ:πΌβΆβ0) |
7 | 6 | adantr 482 |
. . . . . . . 8
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β πΉ:πΌβΆβ0) |
8 | 7 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (πΉβπ) β
β0) |
9 | 3 | ssrab3 4041 |
. . . . . . . . . . . 12
β’ π β π· |
10 | 9 | sseli 3941 |
. . . . . . . . . . 11
β’ (π§ β π β π§ β π·) |
11 | 10 | adantl 483 |
. . . . . . . . . 10
β’ ((πΉ β π· β§ π§ β π) β π§ β π·) |
12 | 2 | psrbagf 21336 |
. . . . . . . . . 10
β’ (π§ β π· β π§:πΌβΆβ0) |
13 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ ((πΉ β π· β§ π§ β π) β π§:πΌβΆβ0) |
14 | 13 | adantrl 715 |
. . . . . . . 8
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β π§:πΌβΆβ0) |
15 | 14 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π§βπ) β
β0) |
16 | | simprl 770 |
. . . . . . . . . 10
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β π₯ β π) |
17 | 9, 16 | sselid 3943 |
. . . . . . . . 9
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β π₯ β π·) |
18 | 2 | psrbagf 21336 |
. . . . . . . . 9
β’ (π₯ β π· β π₯:πΌβΆβ0) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β π₯:πΌβΆβ0) |
20 | 19 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π₯βπ) β
β0) |
21 | | nn0cn 12428 |
. . . . . . . 8
β’ ((πΉβπ) β β0 β (πΉβπ) β β) |
22 | | nn0cn 12428 |
. . . . . . . 8
β’ ((π§βπ) β β0 β (π§βπ) β β) |
23 | | nn0cn 12428 |
. . . . . . . 8
β’ ((π₯βπ) β β0 β (π₯βπ) β β) |
24 | | subsub23 11411 |
. . . . . . . 8
β’ (((πΉβπ) β β β§ (π§βπ) β β β§ (π₯βπ) β β) β (((πΉβπ) β (π§βπ)) = (π₯βπ) β ((πΉβπ) β (π₯βπ)) = (π§βπ))) |
25 | 21, 22, 23, 24 | syl3an 1161 |
. . . . . . 7
β’ (((πΉβπ) β β0 β§ (π§βπ) β β0 β§ (π₯βπ) β β0) β (((πΉβπ) β (π§βπ)) = (π₯βπ) β ((πΉβπ) β (π₯βπ)) = (π§βπ))) |
26 | 8, 15, 20, 25 | syl3anc 1372 |
. . . . . 6
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (((πΉβπ) β (π§βπ)) = (π₯βπ) β ((πΉβπ) β (π₯βπ)) = (π§βπ))) |
27 | | eqcom 2740 |
. . . . . 6
β’ ((π₯βπ) = ((πΉβπ) β (π§βπ)) β ((πΉβπ) β (π§βπ)) = (π₯βπ)) |
28 | | eqcom 2740 |
. . . . . 6
β’ ((π§βπ) = ((πΉβπ) β (π₯βπ)) β ((πΉβπ) β (π₯βπ)) = (π§βπ)) |
29 | 26, 27, 28 | 3bitr4g 314 |
. . . . 5
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π₯βπ) = ((πΉβπ) β (π§βπ)) β (π§βπ) = ((πΉβπ) β (π₯βπ)))) |
30 | 6 | ffnd 6670 |
. . . . . . . 8
β’ (πΉ β π· β πΉ Fn πΌ) |
31 | 30 | adantr 482 |
. . . . . . 7
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β πΉ Fn πΌ) |
32 | 13 | ffnd 6670 |
. . . . . . . 8
β’ ((πΉ β π· β§ π§ β π) β π§ Fn πΌ) |
33 | 32 | adantrl 715 |
. . . . . . 7
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β π§ Fn πΌ) |
34 | 19 | ffnd 6670 |
. . . . . . . 8
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β π₯ Fn πΌ) |
35 | 16, 34 | fndmexd 7844 |
. . . . . . 7
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β πΌ β V) |
36 | | inidm 4179 |
. . . . . . 7
β’ (πΌ β© πΌ) = πΌ |
37 | | eqidd 2734 |
. . . . . . 7
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (πΉβπ) = (πΉβπ)) |
38 | | eqidd 2734 |
. . . . . . 7
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π§βπ) = (π§βπ)) |
39 | 31, 33, 35, 35, 36, 37, 38 | ofval 7629 |
. . . . . 6
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((πΉ βf β π§)βπ) = ((πΉβπ) β (π§βπ))) |
40 | 39 | eqeq2d 2744 |
. . . . 5
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π₯βπ) = ((πΉ βf β π§)βπ) β (π₯βπ) = ((πΉβπ) β (π§βπ)))) |
41 | | eqidd 2734 |
. . . . . . 7
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β (π₯βπ) = (π₯βπ)) |
42 | 31, 34, 35, 35, 36, 37, 41 | ofval 7629 |
. . . . . 6
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((πΉ βf β π₯)βπ) = ((πΉβπ) β (π₯βπ))) |
43 | 42 | eqeq2d 2744 |
. . . . 5
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π§βπ) = ((πΉ βf β π₯)βπ) β (π§βπ) = ((πΉβπ) β (π₯βπ)))) |
44 | 29, 40, 43 | 3bitr4d 311 |
. . . 4
β’ (((πΉ β π· β§ (π₯ β π β§ π§ β π)) β§ π β πΌ) β ((π₯βπ) = ((πΉ βf β π§)βπ) β (π§βπ) = ((πΉ βf β π₯)βπ))) |
45 | 44 | ralbidva 3169 |
. . 3
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (βπ β πΌ (π₯βπ) = ((πΉ βf β π§)βπ) β βπ β πΌ (π§βπ) = ((πΉ βf β π₯)βπ))) |
46 | 5 | adantrl 715 |
. . . . . . 7
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§) β π) |
47 | 9, 46 | sselid 3943 |
. . . . . 6
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§) β π·) |
48 | 2 | psrbagf 21336 |
. . . . . 6
β’ ((πΉ βf β
π§) β π· β (πΉ βf β π§):πΌβΆβ0) |
49 | 47, 48 | syl 17 |
. . . . 5
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§):πΌβΆβ0) |
50 | 49 | ffnd 6670 |
. . . 4
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π§) Fn πΌ) |
51 | | eqfnfv 6983 |
. . . 4
β’ ((π₯ Fn πΌ β§ (πΉ βf β π§) Fn πΌ) β (π₯ = (πΉ βf β π§) β βπ β πΌ (π₯βπ) = ((πΉ βf β π§)βπ))) |
52 | 34, 50, 51 | syl2anc 585 |
. . 3
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (π₯ = (πΉ βf β π§) β βπ β πΌ (π₯βπ) = ((πΉ βf β π§)βπ))) |
53 | 9, 4 | sselid 3943 |
. . . . . . 7
β’ ((πΉ β π· β§ π₯ β π) β (πΉ βf β π₯) β π·) |
54 | 2 | psrbagf 21336 |
. . . . . . 7
β’ ((πΉ βf β
π₯) β π· β (πΉ βf β π₯):πΌβΆβ0) |
55 | 53, 54 | syl 17 |
. . . . . 6
β’ ((πΉ β π· β§ π₯ β π) β (πΉ βf β π₯):πΌβΆβ0) |
56 | 55 | ffnd 6670 |
. . . . 5
β’ ((πΉ β π· β§ π₯ β π) β (πΉ βf β π₯) Fn πΌ) |
57 | 56 | adantrr 716 |
. . . 4
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (πΉ βf β π₯) Fn πΌ) |
58 | | eqfnfv 6983 |
. . . 4
β’ ((π§ Fn πΌ β§ (πΉ βf β π₯) Fn πΌ) β (π§ = (πΉ βf β π₯) β βπ β πΌ (π§βπ) = ((πΉ βf β π₯)βπ))) |
59 | 33, 57, 58 | syl2anc 585 |
. . 3
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (π§ = (πΉ βf β π₯) β βπ β πΌ (π§βπ) = ((πΉ βf β π₯)βπ))) |
60 | 45, 52, 59 | 3bitr4d 311 |
. 2
β’ ((πΉ β π· β§ (π₯ β π β§ π§ β π)) β (π₯ = (πΉ βf β π§) β π§ = (πΉ βf β π₯))) |
61 | 1, 4, 5, 60 | f1o2d 7608 |
1
β’ (πΉ β π· β (π₯ β π β¦ (πΉ βf β π₯)):πβ1-1-ontoβπ) |