Step | Hyp | Ref
| Expression |
1 | | fmfnfm.b |
. . . . . 6
β’ (π β π΅ β (fBasβπ)) |
2 | | fbsspw 23199 |
. . . . . 6
β’ (π΅ β (fBasβπ) β π΅ β π« π) |
3 | 1, 2 | syl 17 |
. . . . 5
β’ (π β π΅ β π« π) |
4 | | elfvdm 6884 |
. . . . . . . 8
β’ (π΅ β (fBasβπ) β π β dom fBas) |
5 | 1, 4 | syl 17 |
. . . . . . 7
β’ (π β π β dom fBas) |
6 | | fmfnfm.l |
. . . . . . 7
β’ (π β πΏ β (Filβπ)) |
7 | | fmfnfm.f |
. . . . . . 7
β’ (π β πΉ:πβΆπ) |
8 | | fmfnfm.fm |
. . . . . . . 8
β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) |
9 | | ffn 6673 |
. . . . . . . . . . 11
β’ (πΉ:πβΆπ β πΉ Fn π) |
10 | | dffn4 6767 |
. . . . . . . . . . 11
β’ (πΉ Fn π β πΉ:πβontoβran πΉ) |
11 | 9, 10 | sylib 217 |
. . . . . . . . . 10
β’ (πΉ:πβΆπ β πΉ:πβontoβran πΉ) |
12 | | foima 6766 |
. . . . . . . . . 10
β’ (πΉ:πβontoβran πΉ β (πΉ β π) = ran πΉ) |
13 | 7, 11, 12 | 3syl 18 |
. . . . . . . . 9
β’ (π β (πΉ β π) = ran πΉ) |
14 | | filtop 23222 |
. . . . . . . . . . 11
β’ (πΏ β (Filβπ) β π β πΏ) |
15 | 6, 14 | syl 17 |
. . . . . . . . . 10
β’ (π β π β πΏ) |
16 | | fgcl 23245 |
. . . . . . . . . . 11
β’ (π΅ β (fBasβπ) β (πfilGenπ΅) β (Filβπ)) |
17 | | filtop 23222 |
. . . . . . . . . . 11
β’ ((πfilGenπ΅) β (Filβπ) β π β (πfilGenπ΅)) |
18 | 1, 16, 17 | 3syl 18 |
. . . . . . . . . 10
β’ (π β π β (πfilGenπ΅)) |
19 | | eqid 2737 |
. . . . . . . . . . 11
β’ (πfilGenπ΅) = (πfilGenπ΅) |
20 | 19 | imaelfm 23318 |
. . . . . . . . . 10
β’ (((π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β (πfilGenπ΅)) β (πΉ β π) β ((π FilMap πΉ)βπ΅)) |
21 | 15, 1, 7, 18, 20 | syl31anc 1374 |
. . . . . . . . 9
β’ (π β (πΉ β π) β ((π FilMap πΉ)βπ΅)) |
22 | 13, 21 | eqeltrrd 2839 |
. . . . . . . 8
β’ (π β ran πΉ β ((π FilMap πΉ)βπ΅)) |
23 | 8, 22 | sseldd 3950 |
. . . . . . 7
β’ (π β ran πΉ β πΏ) |
24 | | rnelfmlem 23319 |
. . . . . . 7
β’ (((π β dom fBas β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ ran πΉ β πΏ) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fBasβπ)) |
25 | 5, 6, 7, 23, 24 | syl31anc 1374 |
. . . . . 6
β’ (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fBasβπ)) |
26 | | fbsspw 23199 |
. . . . . 6
β’ (ran
(π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fBasβπ) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β π« π) |
27 | 25, 26 | syl 17 |
. . . . 5
β’ (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β π« π) |
28 | 3, 27 | unssd 4151 |
. . . 4
β’ (π β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β π« π) |
29 | | ssun1 4137 |
. . . . 5
β’ π΅ β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) |
30 | | fbasne0 23197 |
. . . . . 6
β’ (π΅ β (fBasβπ) β π΅ β β
) |
31 | 1, 30 | syl 17 |
. . . . 5
β’ (π β π΅ β β
) |
32 | | ssn0 4365 |
. . . . 5
β’ ((π΅ β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β§ π΅ β β
) β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β β
) |
33 | 29, 31, 32 | sylancr 588 |
. . . 4
β’ (π β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β β
) |
34 | | eqid 2737 |
. . . . . . . . . 10
β’ (π₯ β πΏ β¦ (β‘πΉ β π₯)) = (π₯ β πΏ β¦ (β‘πΉ β π₯)) |
35 | 34 | elrnmpt 5916 |
. . . . . . . . 9
β’ (π‘ β V β (π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π‘ = (β‘πΉ β π₯))) |
36 | 35 | elv 3454 |
. . . . . . . 8
β’ (π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π‘ = (β‘πΉ β π₯)) |
37 | | 0nelfil 23216 |
. . . . . . . . . . . . . 14
β’ (πΏ β (Filβπ) β Β¬ β
β
πΏ) |
38 | 6, 37 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β Β¬ β
β πΏ) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β Β¬ β
β πΏ) |
40 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΅) β πΏ β (Filβπ)) |
41 | 8 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΅) β ((π FilMap πΉ)βπ΅) β πΏ) |
42 | 15, 1, 7 | 3jca 1129 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ)) |
43 | 42 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΅) β (π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ)) |
44 | | ssfg 23239 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΅ β (fBasβπ) β π΅ β (πfilGenπ΅)) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΅ β (πfilGenπ΅)) |
46 | 45 | sselda 3949 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β π΅) β π β (πfilGenπ΅)) |
47 | 19 | imaelfm 23318 |
. . . . . . . . . . . . . . . . 17
β’ (((π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β (πfilGenπ΅)) β (πΉ β π ) β ((π FilMap πΉ)βπ΅)) |
48 | 43, 46, 47 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β π΅) β (πΉ β π ) β ((π FilMap πΉ)βπ΅)) |
49 | 41, 48 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π΅) β (πΉ β π ) β πΏ) |
50 | 40, 49 | jca 513 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π΅) β (πΏ β (Filβπ) β§ (πΉ β π ) β πΏ)) |
51 | | filin 23221 |
. . . . . . . . . . . . . . 15
β’ ((πΏ β (Filβπ) β§ (πΉ β π ) β πΏ β§ π₯ β πΏ) β ((πΉ β π ) β© π₯) β πΏ) |
52 | 51 | 3expa 1119 |
. . . . . . . . . . . . . 14
β’ (((πΏ β (Filβπ) β§ (πΉ β π ) β πΏ) β§ π₯ β πΏ) β ((πΉ β π ) β© π₯) β πΏ) |
53 | 50, 52 | sylan 581 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β ((πΉ β π ) β© π₯) β πΏ) |
54 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (((πΉ β π ) β© π₯) = β
β (((πΉ β π ) β© π₯) β πΏ β β
β πΏ)) |
55 | 53, 54 | syl5ibcom 244 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (((πΉ β π ) β© π₯) = β
β β
β πΏ)) |
56 | 39, 55 | mtod 197 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β Β¬ ((πΉ β π ) β© π₯) = β
) |
57 | | neq0 4310 |
. . . . . . . . . . . 12
β’ (Β¬
((πΉ β π ) β© π₯) = β
β βπ‘ π‘ β ((πΉ β π ) β© π₯)) |
58 | | elin 3931 |
. . . . . . . . . . . . . 14
β’ (π‘ β ((πΉ β π ) β© π₯) β (π‘ β (πΉ β π ) β§ π‘ β π₯)) |
59 | | ffun 6676 |
. . . . . . . . . . . . . . . . . 18
β’ (πΉ:πβΆπ β Fun πΉ) |
60 | | fvelima 6913 |
. . . . . . . . . . . . . . . . . . 19
β’ ((Fun
πΉ β§ π‘ β (πΉ β π )) β βπ¦ β π (πΉβπ¦) = π‘) |
61 | 60 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (Fun
πΉ β (π‘ β (πΉ β π ) β βπ¦ β π (πΉβπ¦) = π‘)) |
62 | 7, 59, 61 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π‘ β (πΉ β π ) β βπ¦ β π (πΉβπ¦) = π‘)) |
63 | 62 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (π‘ β (πΉ β π ) β βπ¦ β π (πΉβπ¦) = π‘)) |
64 | 7, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β Fun πΉ) |
65 | 64 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π΅) β§ π₯ β πΏ) β§ π¦ β π ) β Fun πΉ) |
66 | | fbelss 23200 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π΅ β (fBasβπ) β§ π β π΅) β π β π) |
67 | 1, 66 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π΅) β π β π) |
68 | 7 | fdmd 6684 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β dom πΉ = π) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π΅) β dom πΉ = π) |
70 | 67, 69 | sseqtrrd 3990 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π΅) β π β dom πΉ) |
71 | 70 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β π β dom πΉ) |
72 | 71 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β π΅) β§ π₯ β πΏ) β§ π¦ β π ) β π¦ β dom πΉ) |
73 | | fvimacnv 7008 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β ((πΉβπ¦) β π₯ β π¦ β (β‘πΉ β π₯))) |
74 | 65, 72, 73 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π΅) β§ π₯ β πΏ) β§ π¦ β π ) β ((πΉβπ¦) β π₯ β π¦ β (β‘πΉ β π₯))) |
75 | | inelcm 4429 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β π β§ π¦ β (β‘πΉ β π₯)) β (π β© (β‘πΉ β π₯)) β β
) |
76 | 75 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π¦ β π β (π¦ β (β‘πΉ β π₯) β (π β© (β‘πΉ β π₯)) β β
)) |
77 | 76 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β π΅) β§ π₯ β πΏ) β§ π¦ β π ) β (π¦ β (β‘πΉ β π₯) β (π β© (β‘πΉ β π₯)) β β
)) |
78 | 74, 77 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β π΅) β§ π₯ β πΏ) β§ π¦ β π ) β ((πΉβπ¦) β π₯ β (π β© (β‘πΉ β π₯)) β β
)) |
79 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ¦) = π‘ β ((πΉβπ¦) β π₯ β π‘ β π₯)) |
80 | 79 | imbi1d 342 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΉβπ¦) = π‘ β (((πΉβπ¦) β π₯ β (π β© (β‘πΉ β π₯)) β β
) β (π‘ β π₯ β (π β© (β‘πΉ β π₯)) β β
))) |
81 | 78, 80 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β π΅) β§ π₯ β πΏ) β§ π¦ β π ) β ((πΉβπ¦) = π‘ β (π‘ β π₯ β (π β© (β‘πΉ β π₯)) β β
))) |
82 | 81 | rexlimdva 3153 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (βπ¦ β π (πΉβπ¦) = π‘ β (π‘ β π₯ β (π β© (β‘πΉ β π₯)) β β
))) |
83 | 63, 82 | syld 47 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (π‘ β (πΉ β π ) β (π‘ β π₯ β (π β© (β‘πΉ β π₯)) β β
))) |
84 | 83 | impd 412 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β ((π‘ β (πΉ β π ) β§ π‘ β π₯) β (π β© (β‘πΉ β π₯)) β β
)) |
85 | 58, 84 | biimtrid 241 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (π‘ β ((πΉ β π ) β© π₯) β (π β© (β‘πΉ β π₯)) β β
)) |
86 | 85 | exlimdv 1937 |
. . . . . . . . . . . 12
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (βπ‘ π‘ β ((πΉ β π ) β© π₯) β (π β© (β‘πΉ β π₯)) β β
)) |
87 | 57, 86 | biimtrid 241 |
. . . . . . . . . . 11
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (Β¬ ((πΉ β π ) β© π₯) = β
β (π β© (β‘πΉ β π₯)) β β
)) |
88 | 56, 87 | mpd 15 |
. . . . . . . . . 10
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (π β© (β‘πΉ β π₯)) β β
) |
89 | | ineq2 4171 |
. . . . . . . . . . 11
β’ (π‘ = (β‘πΉ β π₯) β (π β© π‘) = (π β© (β‘πΉ β π₯))) |
90 | 89 | neeq1d 3004 |
. . . . . . . . . 10
β’ (π‘ = (β‘πΉ β π₯) β ((π β© π‘) β β
β (π β© (β‘πΉ β π₯)) β β
)) |
91 | 88, 90 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π₯ β πΏ) β (π‘ = (β‘πΉ β π₯) β (π β© π‘) β β
)) |
92 | 91 | rexlimdva 3153 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (βπ₯ β πΏ π‘ = (β‘πΉ β π₯) β (π β© π‘) β β
)) |
93 | 36, 92 | biimtrid 241 |
. . . . . . 7
β’ ((π β§ π β π΅) β (π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (π β© π‘) β β
)) |
94 | 93 | expimpd 455 |
. . . . . 6
β’ (π β ((π β π΅ β§ π‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β (π β© π‘) β β
)) |
95 | 94 | ralrimivv 3196 |
. . . . 5
β’ (π β βπ β π΅ βπ‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))(π β© π‘) β β
) |
96 | | fbunfip 23236 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fBasβπ)) β (Β¬ β
β
(fiβ(π΅ βͺ ran
(π₯ β πΏ β¦ (β‘πΉ β π₯)))) β βπ β π΅ βπ‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))(π β© π‘) β β
)) |
97 | 1, 25, 96 | syl2anc 585 |
. . . . 5
β’ (π β (Β¬ β
β
(fiβ(π΅ βͺ ran
(π₯ β πΏ β¦ (β‘πΉ β π₯)))) β βπ β π΅ βπ‘ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))(π β© π‘) β β
)) |
98 | 95, 97 | mpbird 257 |
. . . 4
β’ (π β Β¬ β
β
(fiβ(π΅ βͺ ran
(π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
99 | | fsubbas 23234 |
. . . . 5
β’ (π β dom fBas β
((fiβ(π΅ βͺ ran
(π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ) β ((π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β π« π β§ (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β β
β§ Β¬ β
β
(fiβ(π΅ βͺ ran
(π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
100 | 1, 4, 99 | 3syl 18 |
. . . 4
β’ (π β ((fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ) β ((π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β π« π β§ (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β β
β§ Β¬ β
β
(fiβ(π΅ βͺ ran
(π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
101 | 28, 33, 98, 100 | mpbir3and 1343 |
. . 3
β’ (π β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ)) |
102 | | fgcl 23245 |
. . 3
β’
((fiβ(π΅ βͺ
ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ) β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (Filβπ)) |
103 | 101, 102 | syl 17 |
. 2
β’ (π β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (Filβπ)) |
104 | | unexg 7688 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fBasβπ)) β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V) |
105 | 1, 25, 104 | syl2anc 585 |
. . . . 5
β’ (π β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V) |
106 | | ssfii 9362 |
. . . . 5
β’ ((π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
107 | 105, 106 | syl 17 |
. . . 4
β’ (π β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
108 | 107 | unssad 4152 |
. . 3
β’ (π β π΅ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
109 | | ssfg 23239 |
. . . 4
β’
((fiβ(π΅ βͺ
ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))))) |
110 | 101, 109 | syl 17 |
. . 3
β’ (π β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))))) |
111 | 108, 110 | sstrd 3959 |
. 2
β’ (π β π΅ β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))))) |
112 | 1, 6, 7, 8 | fmfnfmlem4 23324 |
. . . . 5
β’ (π β (π‘ β πΏ β (π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘))) |
113 | | elfm 23314 |
. . . . . 6
β’ ((π β πΏ β§ (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ) β§ πΉ:πβΆπ) β (π‘ β ((π FilMap πΉ)β(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘))) |
114 | 15, 101, 7, 113 | syl3anc 1372 |
. . . . 5
β’ (π β (π‘ β ((π FilMap πΉ)β(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘))) |
115 | 112, 114 | bitr4d 282 |
. . . 4
β’ (π β (π‘ β πΏ β π‘ β ((π FilMap πΉ)β(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
116 | 115 | eqrdv 2735 |
. . 3
β’ (π β πΏ = ((π FilMap πΉ)β(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))))) |
117 | | eqid 2737 |
. . . . 5
β’ (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) = (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
118 | 117 | fmfg 23316 |
. . . 4
β’ ((π β πΏ β§ (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (fBasβπ) β§ πΉ:πβΆπ) β ((π FilMap πΉ)β(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
119 | 15, 101, 7, 118 | syl3anc 1372 |
. . 3
β’ (π β ((π FilMap πΉ)β(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
120 | 116, 119 | eqtrd 2777 |
. 2
β’ (π β πΏ = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
121 | | sseq2 3975 |
. . . 4
β’ (π = (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (π΅ β π β π΅ β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
122 | | fveq2 6847 |
. . . . 5
β’ (π = (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β ((π FilMap πΉ)βπ) = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))) |
123 | 122 | eqeq2d 2748 |
. . . 4
β’ (π = (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (πΏ = ((π FilMap πΉ)βπ) β πΏ = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))))))) |
124 | 121, 123 | anbi12d 632 |
. . 3
β’ (π = (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β ((π΅ β π β§ πΏ = ((π FilMap πΉ)βπ)) β (π΅ β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β§ πΏ = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))))))) |
125 | 124 | rspcev 3584 |
. 2
β’ (((πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (Filβπ) β§ (π΅ β (πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β§ πΏ = ((π FilMap πΉ)β(πfilGen(fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))))))) β βπ β (Filβπ)(π΅ β π β§ πΏ = ((π FilMap πΉ)βπ))) |
126 | 103, 111,
120, 125 | syl12anc 836 |
1
β’ (π β βπ β (Filβπ)(π΅ β π β§ πΏ = ((π FilMap πΉ)βπ))) |