Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . . . 6
β’ (π β πΏ β (Filβπ)) |
2 | 1 | ad2antrr 723 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β πΏ β (Filβπ)) |
3 | | simplr 766 |
. . . . . 6
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β π₯ β πΏ) |
4 | | fmfnfm.fm |
. . . . . . . 8
β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) |
5 | | fmfnfm.f |
. . . . . . . . . 10
β’ (π β πΉ:πβΆπ) |
6 | | ffn 6718 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β πΉ Fn π) |
7 | | dffn4 6812 |
. . . . . . . . . . 11
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
8 | 6, 7 | sylib 217 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β πΉ:πβontoβran πΉ) |
9 | | foima 6811 |
. . . . . . . . . 10
β’ (πΉ:πβontoβran πΉ β (πΉ β π) = ran πΉ) |
10 | 5, 8, 9 | 3syl 18 |
. . . . . . . . 9
β’ (π β (πΉ β π) = ran πΉ) |
11 | | filtop 23580 |
. . . . . . . . . . 11
β’ (πΏ β (Filβπ) β π β πΏ) |
12 | 1, 11 | syl 17 |
. . . . . . . . . 10
β’ (π β π β πΏ) |
13 | | fmfnfm.b |
. . . . . . . . . 10
β’ (π β π΅ β (fBasβπ)) |
14 | | fgcl 23603 |
. . . . . . . . . . 11
β’ (π΅ β (fBasβπ) β (πfilGenπ΅) β (Filβπ)) |
15 | | filtop 23580 |
. . . . . . . . . . 11
β’ ((πfilGenπ΅) β (Filβπ) β π β (πfilGenπ΅)) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π β (πfilGenπ΅)) |
17 | | eqid 2731 |
. . . . . . . . . . 11
β’ (πfilGenπ΅) = (πfilGenπ΅) |
18 | 17 | imaelfm 23676 |
. . . . . . . . . 10
β’ (((π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β (πfilGenπ΅)) β (πΉ β π) β ((π FilMap πΉ)βπ΅)) |
19 | 12, 13, 5, 16, 18 | syl31anc 1372 |
. . . . . . . . 9
β’ (π β (πΉ β π) β ((π FilMap πΉ)βπ΅)) |
20 | 10, 19 | eqeltrrd 2833 |
. . . . . . . 8
β’ (π β ran πΉ β ((π FilMap πΉ)βπ΅)) |
21 | 4, 20 | sseldd 3984 |
. . . . . . 7
β’ (π β ran πΉ β πΏ) |
22 | 21 | ad2antrr 723 |
. . . . . 6
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β ran πΉ β πΏ) |
23 | | filin 23579 |
. . . . . 6
β’ ((πΏ β (Filβπ) β§ π₯ β πΏ β§ ran πΉ β πΏ) β (π₯ β© ran πΉ) β πΏ) |
24 | 2, 3, 22, 23 | syl3anc 1370 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β (π₯ β© ran πΉ) β πΏ) |
25 | | simprr 770 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β π‘ β π) |
26 | | elin 3965 |
. . . . . . 7
β’ (π¦ β (π₯ β© ran πΉ) β (π¦ β π₯ β§ π¦ β ran πΉ)) |
27 | | fvelrnb 6953 |
. . . . . . . . . . . 12
β’ (πΉ Fn π β (π¦ β ran πΉ β βπ§ β π (πΉβπ§) = π¦)) |
28 | 5, 6, 27 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (π¦ β ran πΉ β βπ§ β π (πΉβπ§) = π¦)) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (π¦ β ran πΉ β βπ§ β π (πΉβπ§) = π¦)) |
30 | 5 | ffund 6722 |
. . . . . . . . . . . . . . . 16
β’ (π β Fun πΉ) |
31 | 30 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β Fun πΉ) |
32 | | simprr 770 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β π§ β π) |
33 | 5 | fdmd 6729 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom πΉ = π) |
34 | 33 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β dom πΉ = π) |
35 | 32, 34 | eleqtrrd 2835 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β π§ β dom πΉ) |
36 | | fvimacnv 7055 |
. . . . . . . . . . . . . . 15
β’ ((Fun
πΉ β§ π§ β dom πΉ) β ((πΉβπ§) β π₯ β π§ β (β‘πΉ β π₯))) |
37 | 31, 35, 36 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) β π₯ β π§ β (β‘πΉ β π₯))) |
38 | | cnvimass 6081 |
. . . . . . . . . . . . . . . 16
β’ (β‘πΉ β π₯) β dom πΉ |
39 | | funfvima2 7236 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
πΉ β§ (β‘πΉ β π₯) β dom πΉ) β (π§ β (β‘πΉ β π₯) β (πΉβπ§) β (πΉ β (β‘πΉ β π₯)))) |
40 | 31, 38, 39 | sylancl 585 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β (π§ β (β‘πΉ β π₯) β (πΉβπ§) β (πΉ β (β‘πΉ β π₯)))) |
41 | | ssel 3976 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β (β‘πΉ β π₯)) β π‘ β ((πΉβπ§) β (πΉ β (β‘πΉ β π₯)) β (πΉβπ§) β π‘)) |
42 | 41 | ad2antrl 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) β (πΉ β (β‘πΉ β π₯)) β (πΉβπ§) β π‘)) |
43 | 40, 42 | syld 47 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β (π§ β (β‘πΉ β π₯) β (πΉβπ§) β π‘)) |
44 | 37, 43 | sylbid 239 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) β π₯ β (πΉβπ§) β π‘)) |
45 | | eleq1 2820 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ§) = π¦ β ((πΉβπ§) β π₯ β π¦ β π₯)) |
46 | | eleq1 2820 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ§) = π¦ β ((πΉβπ§) β π‘ β π¦ β π‘)) |
47 | 45, 46 | imbi12d 343 |
. . . . . . . . . . . . 13
β’ ((πΉβπ§) = π¦ β (((πΉβπ§) β π₯ β (πΉβπ§) β π‘) β (π¦ β π₯ β π¦ β π‘))) |
48 | 44, 47 | syl5ibcom 244 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) = π¦ β (π¦ β π₯ β π¦ β π‘))) |
49 | 48 | expr 456 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (π§ β π β ((πΉβπ§) = π¦ β (π¦ β π₯ β π¦ β π‘)))) |
50 | 49 | rexlimdv 3152 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (βπ§ β π (πΉβπ§) = π¦ β (π¦ β π₯ β π¦ β π‘))) |
51 | 29, 50 | sylbid 239 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (π¦ β ran πΉ β (π¦ β π₯ β π¦ β π‘))) |
52 | 51 | impcomd 411 |
. . . . . . . 8
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β ((π¦ β π₯ β§ π¦ β ran πΉ) β π¦ β π‘)) |
53 | 52 | adantrr 714 |
. . . . . . 7
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β ((π¦ β π₯ β§ π¦ β ran πΉ) β π¦ β π‘)) |
54 | 26, 53 | biimtrid 241 |
. . . . . 6
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β (π¦ β (π₯ β© ran πΉ) β π¦ β π‘)) |
55 | 54 | ssrdv 3989 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β (π₯ β© ran πΉ) β π‘) |
56 | | filss 23578 |
. . . . 5
β’ ((πΏ β (Filβπ) β§ ((π₯ β© ran πΉ) β πΏ β§ π‘ β π β§ (π₯ β© ran πΉ) β π‘)) β π‘ β πΏ) |
57 | 2, 24, 25, 55, 56 | syl13anc 1371 |
. . . 4
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β π‘ β πΏ) |
58 | 57 | exp32 420 |
. . 3
β’ ((π β§ π₯ β πΏ) β ((πΉ β (β‘πΉ β π₯)) β π‘ β (π‘ β π β π‘ β πΏ))) |
59 | | imaeq2 6056 |
. . . . 5
β’ (π = (β‘πΉ β π₯) β (πΉ β π ) = (πΉ β (β‘πΉ β π₯))) |
60 | 59 | sseq1d 4014 |
. . . 4
β’ (π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (πΉ β (β‘πΉ β π₯)) β π‘)) |
61 | 60 | imbi1d 340 |
. . 3
β’ (π = (β‘πΉ β π₯) β (((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)) β ((πΉ β (β‘πΉ β π₯)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
62 | 58, 61 | syl5ibrcom 246 |
. 2
β’ ((π β§ π₯ β πΏ) β (π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
63 | 62 | rexlimdva 3154 |
1
β’ (π β (βπ₯ β πΏ π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |