Step | Hyp | Ref
| Expression |
1 | | fmfnfm.l |
. . . 4
β’ (π β πΏ β (Filβπ)) |
2 | | filelss 23219 |
. . . . 5
β’ ((πΏ β (Filβπ) β§ π‘ β πΏ) β π‘ β π) |
3 | 2 | ex 414 |
. . . 4
β’ (πΏ β (Filβπ) β (π‘ β πΏ β π‘ β π)) |
4 | 1, 3 | syl 17 |
. . 3
β’ (π β (π‘ β πΏ β π‘ β π)) |
5 | | fmfnfm.b |
. . . . . . . . 9
β’ (π β π΅ β (fBasβπ)) |
6 | | mptexg 7176 |
. . . . . . . . . . 11
β’ (πΏ β (Filβπ) β (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) |
7 | | rnexg 7846 |
. . . . . . . . . . 11
β’ ((π₯ β πΏ β¦ (β‘πΉ β π₯)) β V β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
β’ (πΏ β (Filβπ) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
β’ (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) |
10 | | unexg 7688 |
. . . . . . . . 9
β’ ((π΅ β (fBasβπ) β§ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V) |
11 | 5, 9, 10 | syl2anc 585 |
. . . . . . . 8
β’ (π β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V) |
12 | | ssfii 9362 |
. . . . . . . . 9
β’ ((π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V β (π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
13 | 12 | unssbd 4153 |
. . . . . . . 8
β’ ((π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β V β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
14 | 11, 13 | syl 17 |
. . . . . . 7
β’ (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
15 | 14 | adantr 482 |
. . . . . 6
β’ ((π β§ π‘ β πΏ) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
16 | | eqid 2737 |
. . . . . . . . 9
β’ (β‘πΉ β π‘) = (β‘πΉ β π‘) |
17 | | imaeq2 6014 |
. . . . . . . . . 10
β’ (π₯ = π‘ β (β‘πΉ β π₯) = (β‘πΉ β π‘)) |
18 | 17 | rspceeqv 3600 |
. . . . . . . . 9
β’ ((π‘ β πΏ β§ (β‘πΉ β π‘) = (β‘πΉ β π‘)) β βπ₯ β πΏ (β‘πΉ β π‘) = (β‘πΉ β π₯)) |
19 | 16, 18 | mpan2 690 |
. . . . . . . 8
β’ (π‘ β πΏ β βπ₯ β πΏ (β‘πΉ β π‘) = (β‘πΉ β π₯)) |
20 | 19 | adantl 483 |
. . . . . . 7
β’ ((π β§ π‘ β πΏ) β βπ₯ β πΏ (β‘πΉ β π‘) = (β‘πΉ β π₯)) |
21 | | elfvdm 6884 |
. . . . . . . . . . 11
β’ (π΅ β (fBasβπ) β π β dom fBas) |
22 | 5, 21 | syl 17 |
. . . . . . . . . 10
β’ (π β π β dom fBas) |
23 | | cnvimass 6038 |
. . . . . . . . . . 11
β’ (β‘πΉ β π‘) β dom πΉ |
24 | | fmfnfm.f |
. . . . . . . . . . 11
β’ (π β πΉ:πβΆπ) |
25 | 23, 24 | fssdm 6693 |
. . . . . . . . . 10
β’ (π β (β‘πΉ β π‘) β π) |
26 | 22, 25 | ssexd 5286 |
. . . . . . . . 9
β’ (π β (β‘πΉ β π‘) β V) |
27 | 26 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π‘ β πΏ) β (β‘πΉ β π‘) β V) |
28 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β πΏ β¦ (β‘πΉ β π₯)) = (π₯ β πΏ β¦ (β‘πΉ β π₯)) |
29 | 28 | elrnmpt 5916 |
. . . . . . . 8
β’ ((β‘πΉ β π‘) β V β ((β‘πΉ β π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ (β‘πΉ β π‘) = (β‘πΉ β π₯))) |
30 | 27, 29 | syl 17 |
. . . . . . 7
β’ ((π β§ π‘ β πΏ) β ((β‘πΉ β π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ (β‘πΉ β π‘) = (β‘πΉ β π₯))) |
31 | 20, 30 | mpbird 257 |
. . . . . 6
β’ ((π β§ π‘ β πΏ) β (β‘πΉ β π‘) β ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) |
32 | 15, 31 | sseldd 3950 |
. . . . 5
β’ ((π β§ π‘ β πΏ) β (β‘πΉ β π‘) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) |
33 | | ffun 6676 |
. . . . . . . 8
β’ (πΉ:πβΆπ β Fun πΉ) |
34 | | ssid 3971 |
. . . . . . . 8
β’ (β‘πΉ β π‘) β (β‘πΉ β π‘) |
35 | | funimass2 6589 |
. . . . . . . 8
β’ ((Fun
πΉ β§ (β‘πΉ β π‘) β (β‘πΉ β π‘)) β (πΉ β (β‘πΉ β π‘)) β π‘) |
36 | 33, 34, 35 | sylancl 587 |
. . . . . . 7
β’ (πΉ:πβΆπ β (πΉ β (β‘πΉ β π‘)) β π‘) |
37 | 24, 36 | syl 17 |
. . . . . 6
β’ (π β (πΉ β (β‘πΉ β π‘)) β π‘) |
38 | 37 | adantr 482 |
. . . . 5
β’ ((π β§ π‘ β πΏ) β (πΉ β (β‘πΉ β π‘)) β π‘) |
39 | | imaeq2 6014 |
. . . . . . 7
β’ (π = (β‘πΉ β π‘) β (πΉ β π ) = (πΉ β (β‘πΉ β π‘))) |
40 | 39 | sseq1d 3980 |
. . . . . 6
β’ (π = (β‘πΉ β π‘) β ((πΉ β π ) β π‘ β (πΉ β (β‘πΉ β π‘)) β π‘)) |
41 | 40 | rspcev 3584 |
. . . . 5
β’ (((β‘πΉ β π‘) β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β§ (πΉ β (β‘πΉ β π‘)) β π‘) β βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘) |
42 | 32, 38, 41 | syl2anc 585 |
. . . 4
β’ ((π β§ π‘ β πΏ) β βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘) |
43 | 42 | ex 414 |
. . 3
β’ (π β (π‘ β πΏ β βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘)) |
44 | 4, 43 | jcad 514 |
. 2
β’ (π β (π‘ β πΏ β (π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘))) |
45 | | elfiun 9373 |
. . . . . 6
β’ ((π΅ β (fBasβπ) β§ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β V) β (π β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (π β (fiβπ΅) β¨ π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β¨ βπ§ β (fiβπ΅)βπ€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯)))π = (π§ β© π€)))) |
46 | 5, 9, 45 | syl2anc 585 |
. . . . 5
β’ (π β (π β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β (π β (fiβπ΅) β¨ π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β¨ βπ§ β (fiβπ΅)βπ€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯)))π = (π§ β© π€)))) |
47 | | fmfnfm.fm |
. . . . . . 7
β’ (π β ((π FilMap πΉ)βπ΅) β πΏ) |
48 | 5, 1, 24, 47 | fmfnfmlem1 23321 |
. . . . . 6
β’ (π β (π β (fiβπ΅) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
49 | 5, 1, 24, 47 | fmfnfmlem3 23323 |
. . . . . . . 8
β’ (π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) = ran (π₯ β πΏ β¦ (β‘πΉ β π₯))) |
50 | 49 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) |
51 | 28 | elrnmpt 5916 |
. . . . . . . . 9
β’ (π β V β (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π = (β‘πΉ β π₯))) |
52 | 51 | elv 3454 |
. . . . . . . 8
β’ (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π = (β‘πΉ β π₯)) |
53 | 5, 1, 24, 47 | fmfnfmlem2 23322 |
. . . . . . . 8
β’ (π β (βπ₯ β πΏ π = (β‘πΉ β π₯) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
54 | 52, 53 | biimtrid 241 |
. . . . . . 7
β’ (π β (π β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
55 | 50, 54 | sylbid 239 |
. . . . . 6
β’ (π β (π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
56 | 49 | eleq2d 2824 |
. . . . . . . . . . . 12
β’ (π β (π€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β π€ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) |
57 | 28 | elrnmpt 5916 |
. . . . . . . . . . . . 13
β’ (π€ β V β (π€ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π€ = (β‘πΉ β π₯))) |
58 | 57 | elv 3454 |
. . . . . . . . . . . 12
β’ (π€ β ran (π₯ β πΏ β¦ (β‘πΉ β π₯)) β βπ₯ β πΏ π€ = (β‘πΉ β π₯)) |
59 | 56, 58 | bitrdi 287 |
. . . . . . . . . . 11
β’ (π β (π€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β βπ₯ β πΏ π€ = (β‘πΉ β π₯))) |
60 | 59 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ β (fiβπ΅)) β (π€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β βπ₯ β πΏ π€ = (β‘πΉ β π₯))) |
61 | | fbssfi 23204 |
. . . . . . . . . . . 12
β’ ((π΅ β (fBasβπ) β§ π§ β (fiβπ΅)) β βπ β π΅ π β π§) |
62 | 5, 61 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (fiβπ΅)) β βπ β π΅ π β π§) |
63 | 1 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β πΏ β (Filβπ)) |
64 | 1 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β π΅ β§ π β π§)) β πΏ β (Filβπ)) |
65 | 47 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π΅) β ((π FilMap πΉ)βπ΅) β πΏ) |
66 | | filtop 23222 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (πΏ β (Filβπ) β π β πΏ) |
67 | 1, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β πΏ) |
68 | 67, 5, 24 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ)) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π΅) β (π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ)) |
70 | | ssfg 23239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π΅ β (fBasβπ) β π΅ β (πfilGenπ΅)) |
71 | 5, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β π΅ β (πfilGenπ΅)) |
72 | 71 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β π΅) β π β (πfilGenπ΅)) |
73 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (πfilGenπ΅) = (πfilGenπ΅) |
74 | 73 | imaelfm 23318 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β πΏ β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β§ π β (πfilGenπ΅)) β (πΉ β π ) β ((π FilMap πΉ)βπ΅)) |
75 | 69, 72, 74 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β π΅) β (πΉ β π ) β ((π FilMap πΉ)βπ΅)) |
76 | 65, 75 | sseldd 3950 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π΅) β (πΉ β π ) β πΏ) |
77 | 76 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ (π β π΅ β§ π β π§)) β (πΉ β π ) β πΏ) |
78 | 64, 77 | jca 513 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π β π΅ β§ π β π§)) β (πΏ β (Filβπ) β§ (πΉ β π ) β πΏ)) |
79 | | filin 23221 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΏ β (Filβπ) β§ (πΉ β π ) β πΏ β§ π₯ β πΏ) β ((πΉ β π ) β© π₯) β πΏ) |
80 | 79 | 3expa 1119 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πΏ β (Filβπ) β§ (πΉ β π ) β πΏ) β§ π₯ β πΏ) β ((πΉ β π ) β© π₯) β πΏ) |
81 | 78, 80 | sylan 581 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β ((πΉ β π ) β© π₯) β πΏ) |
82 | 81 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β ((πΉ β π ) β© π₯) β πΏ) |
83 | | simprr 772 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β π‘ β π) |
84 | | elin 3931 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π€ β ((πΉ β π ) β© π₯) β (π€ β (πΉ β π ) β§ π€ β π₯)) |
85 | 24, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β Fun πΉ) |
86 | | fvelima 6913 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((Fun
πΉ β§ π€ β (πΉ β π )) β βπ¦ β π (πΉβπ¦) = π€) |
87 | 86 | ex 414 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (Fun
πΉ β (π€ β (πΉ β π ) β βπ¦ β π (πΉβπ¦) = π€)) |
88 | 85, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (π€ β (πΉ β π ) β βπ¦ β π (πΉβπ¦) = π€)) |
89 | 88 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β (π€ β (πΉ β π ) β βπ¦ β π (πΉβπ¦) = π€)) |
90 | 85 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ (π‘ β π β§ (π¦ β π β§ (πΉβπ¦) β π₯))) β Fun πΉ) |
91 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β π β π§) |
92 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π‘ β π β§ (π¦ β π β§ (πΉβπ¦) β π₯)) β π¦ β π ) |
93 | | ssel2 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β π§ β§ π¦ β π ) β π¦ β π§) |
94 | 91, 92, 93 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ (π‘ β π β§ (π¦ β π β§ (πΉβπ¦) β π₯))) β π¦ β π§) |
95 | 85 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π¦ β π ) β Fun πΉ) |
96 | | fbelss 23200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π΅ β (fBasβπ) β§ π β π΅) β π β π) |
97 | 5, 96 | sylan 581 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ π β π΅) β π β π) |
98 | 24 | fdmd 6684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β dom πΉ = π) |
99 | 98 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β§ π β π΅) β dom πΉ = π) |
100 | 97, 99 | sseqtrrd 3990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ π β π΅) β π β dom πΉ) |
101 | 100 | adantrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β§ (π β π΅ β§ π β π§)) β π β dom πΉ) |
102 | 101 | sselda 3949 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π¦ β π ) β π¦ β dom πΉ) |
103 | | fvimacnv 7008 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((Fun
πΉ β§ π¦ β dom πΉ) β ((πΉβπ¦) β π₯ β π¦ β (β‘πΉ β π₯))) |
104 | 95, 102, 103 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π¦ β π ) β ((πΉβπ¦) β π₯ β π¦ β (β‘πΉ β π₯))) |
105 | 104 | biimpd 228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π¦ β π ) β ((πΉβπ¦) β π₯ β π¦ β (β‘πΉ β π₯))) |
106 | 105 | impr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β§ (π β π΅ β§ π β π§)) β§ (π¦ β π β§ (πΉβπ¦) β π₯)) β π¦ β (β‘πΉ β π₯)) |
107 | 106 | ad2ant2rl 748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ (π‘ β π β§ (π¦ β π β§ (πΉβπ¦) β π₯))) β π¦ β (β‘πΉ β π₯)) |
108 | 94, 107 | elind 4159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ (π‘ β π β§ (π¦ β π β§ (πΉβπ¦) β π₯))) β π¦ β (π§ β© (β‘πΉ β π₯))) |
109 | | inss2 4194 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ β© (β‘πΉ β π₯)) β (β‘πΉ β π₯) |
110 | | cnvimass 6038 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (β‘πΉ β π₯) β dom πΉ |
111 | 109, 110 | sstri 3958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ β© (β‘πΉ β π₯)) β dom πΉ |
112 | | funfvima2 7186 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((Fun
πΉ β§ (π§ β© (β‘πΉ β π₯)) β dom πΉ) β (π¦ β (π§ β© (β‘πΉ β π₯)) β (πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
113 | 111, 112 | mpan2 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (Fun
πΉ β (π¦ β (π§ β© (β‘πΉ β π₯)) β (πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
114 | 90, 108, 113 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ (π‘ β π β§ (π¦ β π β§ (πΉβπ¦) β π₯))) β (πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯)))) |
115 | 114 | anassrs 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β§ (π¦ β π β§ (πΉβπ¦) β π₯)) β (πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯)))) |
116 | 115 | expr 458 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β§ π¦ β π ) β ((πΉβπ¦) β π₯ β (πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
117 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉβπ¦) = π€ β ((πΉβπ¦) β π₯ β π€ β π₯)) |
118 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΉβπ¦) = π€ β ((πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯))) β π€ β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
119 | 117, 118 | imbi12d 345 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((πΉβπ¦) = π€ β (((πΉβπ¦) β π₯ β (πΉβπ¦) β (πΉ β (π§ β© (β‘πΉ β π₯)))) β (π€ β π₯ β π€ β (πΉ β (π§ β© (β‘πΉ β π₯)))))) |
120 | 116, 119 | syl5ibcom 244 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β§ π¦ β π ) β ((πΉβπ¦) = π€ β (π€ β π₯ β π€ β (πΉ β (π§ β© (β‘πΉ β π₯)))))) |
121 | 120 | rexlimdva 3153 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β (βπ¦ β π (πΉβπ¦) = π€ β (π€ β π₯ β π€ β (πΉ β (π§ β© (β‘πΉ β π₯)))))) |
122 | 89, 121 | syld 47 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β (π€ β (πΉ β π ) β (π€ β π₯ β π€ β (πΉ β (π§ β© (β‘πΉ β π₯)))))) |
123 | 122 | impd 412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β ((π€ β (πΉ β π ) β§ π€ β π₯) β π€ β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
124 | 84, 123 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ π‘ β π) β (π€ β ((πΉ β π ) β© π₯) β π€ β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
125 | 124 | adantrl 715 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β (π€ β ((πΉ β π ) β© π₯) β π€ β (πΉ β (π§ β© (β‘πΉ β π₯))))) |
126 | 125 | ssrdv 3955 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β ((πΉ β π ) β© π₯) β (πΉ β (π§ β© (β‘πΉ β π₯)))) |
127 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β (πΉ β (π§ β© (β‘πΉ β π₯))) β π‘) |
128 | 126, 127 | sstrd 3959 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β ((πΉ β π ) β© π₯) β π‘) |
129 | | filss 23220 |
. . . . . . . . . . . . . . . . 17
β’ ((πΏ β (Filβπ) β§ (((πΉ β π ) β© π₯) β πΏ β§ π‘ β π β§ ((πΉ β π ) β© π₯) β π‘)) β π‘ β πΏ) |
130 | 63, 82, 83, 128, 129 | syl13anc 1373 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β§ ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β§ π‘ β π)) β π‘ β πΏ) |
131 | 130 | exp32 422 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β (π‘ β π β π‘ β πΏ))) |
132 | | ineq2 4171 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = (β‘πΉ β π₯) β (π§ β© π€) = (π§ β© (β‘πΉ β π₯))) |
133 | 132 | imaeq2d 6018 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = (β‘πΉ β π₯) β (πΉ β (π§ β© π€)) = (πΉ β (π§ β© (β‘πΉ β π₯)))) |
134 | 133 | sseq1d 3980 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (β‘πΉ β π₯) β ((πΉ β (π§ β© π€)) β π‘ β (πΉ β (π§ β© (β‘πΉ β π₯))) β π‘)) |
135 | 134 | imbi1d 342 |
. . . . . . . . . . . . . . 15
β’ (π€ = (β‘πΉ β π₯) β (((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)) β ((πΉ β (π§ β© (β‘πΉ β π₯))) β π‘ β (π‘ β π β π‘ β πΏ)))) |
136 | 131, 135 | syl5ibrcom 247 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π β π΅ β§ π β π§)) β§ π₯ β πΏ) β (π€ = (β‘πΉ β π₯) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
137 | 136 | rexlimdva 3153 |
. . . . . . . . . . . . 13
β’ ((π β§ (π β π΅ β§ π β π§)) β (βπ₯ β πΏ π€ = (β‘πΉ β π₯) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
138 | 137 | rexlimdvaa 3154 |
. . . . . . . . . . . 12
β’ (π β (βπ β π΅ π β π§ β (βπ₯ β πΏ π€ = (β‘πΉ β π₯) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ))))) |
139 | 138 | imp 408 |
. . . . . . . . . . 11
β’ ((π β§ βπ β π΅ π β π§) β (βπ₯ β πΏ π€ = (β‘πΉ β π₯) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
140 | 62, 139 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π§ β (fiβπ΅)) β (βπ₯ β πΏ π€ = (β‘πΉ β π₯) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
141 | 60, 140 | sylbid 239 |
. . . . . . . . 9
β’ ((π β§ π§ β (fiβπ΅)) β (π€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
142 | 141 | impr 456 |
. . . . . . . 8
β’ ((π β§ (π§ β (fiβπ΅) β§ π€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ))) |
143 | | imaeq2 6014 |
. . . . . . . . . 10
β’ (π = (π§ β© π€) β (πΉ β π ) = (πΉ β (π§ β© π€))) |
144 | 143 | sseq1d 3980 |
. . . . . . . . 9
β’ (π = (π§ β© π€) β ((πΉ β π ) β π‘ β (πΉ β (π§ β© π€)) β π‘)) |
145 | 144 | imbi1d 342 |
. . . . . . . 8
β’ (π = (π§ β© π€) β (((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)) β ((πΉ β (π§ β© π€)) β π‘ β (π‘ β π β π‘ β πΏ)))) |
146 | 142, 145 | syl5ibrcom 247 |
. . . . . . 7
β’ ((π β§ (π§ β (fiβπ΅) β§ π€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))))) β (π = (π§ β© π€) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
147 | 146 | rexlimdvva 3206 |
. . . . . 6
β’ (π β (βπ§ β (fiβπ΅)βπ€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯)))π = (π§ β© π€) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
148 | 48, 55, 147 | 3jaod 1429 |
. . . . 5
β’ (π β ((π β (fiβπ΅) β¨ π β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯))) β¨ βπ§ β (fiβπ΅)βπ€ β (fiβran (π₯ β πΏ β¦ (β‘πΉ β π₯)))π = (π§ β© π€)) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
149 | 46, 148 | sylbid 239 |
. . . 4
β’ (π β (π β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯)))) β ((πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ)))) |
150 | 149 | rexlimdv 3151 |
. . 3
β’ (π β (βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘ β (π‘ β π β π‘ β πΏ))) |
151 | 150 | impcomd 413 |
. 2
β’ (π β ((π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘) β π‘ β πΏ)) |
152 | 44, 151 | impbid 211 |
1
β’ (π β (π‘ β πΏ β (π‘ β π β§ βπ β (fiβ(π΅ βͺ ran (π₯ β πΏ β¦ (β‘πΉ β π₯))))(πΉ β π ) β π‘))) |