Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . . . 6
β’ (π β πΏ β (Filβπ)) |
2 | 1 | ad2antrr 724 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β πΏ β (Filβπ)) |
3 | | simplr 767 |
. . . . . 6
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β π₯ β πΏ) |
4 | | fmfnfm.fm |
. . . . . . . 8
β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) |
5 | | fmfnfm.f |
. . . . . . . . . 10
β’ (π β πΉ:πβΆπ) |
6 | | ffn 6717 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β πΉ Fn π) |
7 | | dffn4 6811 |
. . . . . . . . . . 11
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
8 | 6, 7 | sylib 217 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β πΉ:πβontoβran πΉ) |
9 | | foima 6810 |
. . . . . . . . . 10
β’ (πΉ:πβontoβran πΉ β (πΉ β π) = ran πΉ) |
10 | 5, 8, 9 | 3syl 18 |
. . . . . . . . 9
β’ (π β (πΉ β π) = ran πΉ) |
11 | | filtop 23366 |
. . . . . . . . . . 11
β’ (πΏ β (Filβπ) β π β πΏ) |
12 | 1, 11 | syl 17 |
. . . . . . . . . 10
β’ (π β π β πΏ) |
13 | | fmfnfm.b |
. . . . . . . . . 10
β’ (π β π΅ β (fBasβπ)) |
14 | | fgcl 23389 |
. . . . . . . . . . 11
β’ (π΅ β (fBasβπ) β (πfilGenπ΅) β (Filβπ)) |
15 | | filtop 23366 |
. . . . . . . . . . 11
β’ ((πfilGenπ΅) β (Filβπ) β π β (πfilGenπ΅)) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π β (πfilGenπ΅)) |
17 | | eqid 2732 |
. . . . . . . . . . 11
β’ (πfilGenπ΅) = (πfilGenπ΅) |
18 | 17 | imaelfm 23462 |
. . . . . . . . . 10
β’ (((π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β (πfilGenπ΅)) β (πΉ β π) β ((π FilMap πΉ)βπ΅)) |
19 | 12, 13, 5, 16, 18 | syl31anc 1373 |
. . . . . . . . 9
β’ (π β (πΉ β π) β ((π FilMap πΉ)βπ΅)) |
20 | 10, 19 | eqeltrrd 2834 |
. . . . . . . 8
β’ (π β ran πΉ β ((π FilMap πΉ)βπ΅)) |
21 | 4, 20 | sseldd 3983 |
. . . . . . 7
β’ (π β ran πΉ β πΏ) |
22 | 21 | ad2antrr 724 |
. . . . . 6
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β ran πΉ β πΏ) |
23 | | filin 23365 |
. . . . . 6
β’ ((πΏ β (Filβπ) β§ π₯ β πΏ β§ ran πΉ β πΏ) β (π₯ β© ran πΉ) β πΏ) |
24 | 2, 3, 22, 23 | syl3anc 1371 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β (π₯ β© ran πΉ) β πΏ) |
25 | | simprr 771 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β π‘ β π) |
26 | | elin 3964 |
. . . . . . 7
β’ (π¦ β (π₯ β© ran πΉ) β (π¦ β π₯ β§ π¦ β ran πΉ)) |
27 | | fvelrnb 6952 |
. . . . . . . . . . . 12
β’ (πΉ Fn π β (π¦ β ran πΉ β βπ§ β π (πΉβπ§) = π¦)) |
28 | 5, 6, 27 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β (π¦ β ran πΉ β βπ§ β π (πΉβπ§) = π¦)) |
29 | 28 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (π¦ β ran πΉ β βπ§ β π (πΉβπ§) = π¦)) |
30 | 5 | ffund 6721 |
. . . . . . . . . . . . . . . 16
β’ (π β Fun πΉ) |
31 | 30 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β Fun πΉ) |
32 | | simprr 771 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β π§ β π) |
33 | 5 | fdmd 6728 |
. . . . . . . . . . . . . . . . 17
β’ (π β dom πΉ = π) |
34 | 33 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β dom πΉ = π) |
35 | 32, 34 | eleqtrrd 2836 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β π§ β dom πΉ) |
36 | | fvimacnv 7054 |
. . . . . . . . . . . . . . 15
β’ ((Fun
πΉ β§ π§ β dom πΉ) β ((πΉβπ§) β π₯ β π§ β (β‘πΉ β π₯))) |
37 | 31, 35, 36 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) β π₯ β π§ β (β‘πΉ β π₯))) |
38 | | cnvimass 6080 |
. . . . . . . . . . . . . . . 16
β’ (β‘πΉ β π₯) β dom πΉ |
39 | | funfvima2 7235 |
. . . . . . . . . . . . . . . 16
β’ ((Fun
πΉ β§ (β‘πΉ β π₯) β dom πΉ) β (π§ β (β‘πΉ β π₯) β (πΉβπ§) β (πΉ β (β‘πΉ β π₯)))) |
40 | 31, 38, 39 | sylancl 586 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β (π§ β (β‘πΉ β π₯) β (πΉβπ§) β (πΉ β (β‘πΉ β π₯)))) |
41 | | ssel 3975 |
. . . . . . . . . . . . . . . 16
β’ ((πΉ β (β‘πΉ β π₯)) β π‘ β ((πΉβπ§) β (πΉ β (β‘πΉ β π₯)) β (πΉβπ§) β π‘)) |
42 | 41 | ad2antrl 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) β (πΉ β (β‘πΉ β π₯)) β (πΉβπ§) β π‘)) |
43 | 40, 42 | syld 47 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β (π§ β (β‘πΉ β π₯) β (πΉβπ§) β π‘)) |
44 | 37, 43 | sylbid 239 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) β π₯ β (πΉβπ§) β π‘)) |
45 | | eleq1 2821 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ§) = π¦ β ((πΉβπ§) β π₯ β π¦ β π₯)) |
46 | | eleq1 2821 |
. . . . . . . . . . . . . 14
β’ ((πΉβπ§) = π¦ β ((πΉβπ§) β π‘ β π¦ β π‘)) |
47 | 45, 46 | imbi12d 344 |
. . . . . . . . . . . . 13
β’ ((πΉβπ§) = π¦ β (((πΉβπ§) β π₯ β (πΉβπ§) β π‘) β (π¦ β π₯ β π¦ β π‘))) |
48 | 44, 47 | syl5ibcom 244 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π§ β π)) β ((πΉβπ§) = π¦ β (π¦ β π₯ β π¦ β π‘))) |
49 | 48 | expr 457 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (π§ β π β ((πΉβπ§) = π¦ β (π¦ β π₯ β π¦ β π‘)))) |
50 | 49 | rexlimdv 3153 |
. . . . . . . . . 10
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (βπ§ β π (πΉβπ§) = π¦ β (π¦ β π₯ β π¦ β π‘))) |
51 | 29, 50 | sylbid 239 |
. . . . . . . . 9
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β (π¦ β ran πΉ β (π¦ β π₯ β π¦ β π‘))) |
52 | 51 | impcomd 412 |
. . . . . . . 8
β’ (((π β§ π₯ β πΏ) β§ (πΉ β (β‘πΉ β π₯)) β π‘) β ((π¦ β π₯ β§ π¦ β ran πΉ) β π¦ β π‘)) |
53 | 52 | adantrr 715 |
. . . . . . 7
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β ((π¦ β π₯ β§ π¦ β ran πΉ) β π¦ β π‘)) |
54 | 26, 53 | biimtrid 241 |
. . . . . 6
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β (π¦ β (π₯ β© ran πΉ) β π¦ β π‘)) |
55 | 54 | ssrdv 3988 |
. . . . 5
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β (π₯ β© ran πΉ) β π‘) |
56 | | filss 23364 |
. . . . 5
β’ ((πΏ β (Filβπ) β§ ((π₯ β© ran πΉ) β πΏ β§ π‘ β π β§ (π₯ β© ran πΉ) β π‘)) β π‘ β πΏ) |
57 | 2, 24, 25, 55, 56 | syl13anc 1372 |
. . . 4
β’ (((π β§ π₯ β πΏ) β§ ((πΉ β (β‘πΉ β π₯)) β π‘ β§ π‘ β π)) β π‘ β πΏ) |
58 | 57 | exp32 421 |
. . 3
β’ ((π β§ π₯ β πΏ) β ((πΉ β (β‘πΉ β π₯)) β π‘ β (π‘ β π β π‘ β πΏ))) |
59 | | imaeq2 6055 |
. . . . 5
β’ (π = (β‘πΉ β π₯) β (πΉ β π ) = (πΉ β (β‘πΉ β π₯))) |
60 | 59 | sseq1d 4013 |
. . . 4
β’ (π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (πΉ β (β‘πΉ β π₯)) β π‘)) |
61 | 60 | imbi1d 341 |
. . 3
β’ (π = (β‘πΉ β π₯) β (((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)) β ((πΉ β (β‘πΉ β π₯)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
62 | 58, 61 | syl5ibrcom 246 |
. 2
β’ ((π β§ π₯ β πΏ) β (π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
63 | 62 | rexlimdva 3155 |
1
β’ (π β (βπ₯ β πΏ π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |