Step | Hyp | Ref
| Expression |
1 | | zex 12516 |
. . . . . 6
β’ β€
β V |
2 | 1 | pwex 5339 |
. . . . 5
β’ π«
β€ β V |
3 | | uzf 12774 |
. . . . . 6
β’
β€β₯:β€βΆπ« β€ |
4 | | frn 6679 |
. . . . . 6
β’
(β€β₯:β€βΆπ« β€ β ran
β€β₯ β π« β€) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
β’ ran
β€β₯ β π« β€ |
6 | 2, 5 | ssexi 5283 |
. . . 4
β’ ran
β€β₯ β V |
7 | | uzfbas.1 |
. . . . 5
β’ π =
(β€β₯βπ) |
8 | 7 | fvexi 6860 |
. . . 4
β’ π β V |
9 | | restval 17316 |
. . . 4
β’ ((ran
β€β₯ β V β§ π β V) β (ran
β€β₯ βΎt π) = ran (π₯ β ran β€β₯ β¦
(π₯ β© π))) |
10 | 6, 8, 9 | mp2an 691 |
. . 3
β’ (ran
β€β₯ βΎt π) = ran (π₯ β ran β€β₯ β¦
(π₯ β© π)) |
11 | 7 | ineq2i 4173 |
. . . . . . . . 9
β’
((β€β₯βπ¦) β© π) = ((β€β₯βπ¦) β©
(β€β₯βπ)) |
12 | | uzin 12811 |
. . . . . . . . . 10
β’ ((π¦ β β€ β§ π β β€) β
((β€β₯βπ¦) β© (β€β₯βπ)) =
(β€β₯βif(π¦ β€ π, π, π¦))) |
13 | 12 | ancoms 460 |
. . . . . . . . 9
β’ ((π β β€ β§ π¦ β β€) β
((β€β₯βπ¦) β© (β€β₯βπ)) =
(β€β₯βif(π¦ β€ π, π, π¦))) |
14 | 11, 13 | eqtrid 2785 |
. . . . . . . 8
β’ ((π β β€ β§ π¦ β β€) β
((β€β₯βπ¦) β© π) = (β€β₯βif(π¦ β€ π, π, π¦))) |
15 | | ffn 6672 |
. . . . . . . . . 10
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
16 | 3, 15 | ax-mp 5 |
. . . . . . . . 9
β’
β€β₯ Fn β€ |
17 | | uzssz 12792 |
. . . . . . . . . 10
β’
(β€β₯βπ) β β€ |
18 | 7, 17 | eqsstri 3982 |
. . . . . . . . 9
β’ π β
β€ |
19 | | ifcl 4535 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π¦ β β€) β if(π¦ β€ π, π, π¦) β β€) |
20 | | uzid 12786 |
. . . . . . . . . . . 12
β’ (if(π¦ β€ π, π, π¦) β β€ β if(π¦ β€ π, π, π¦) β
(β€β₯βif(π¦ β€ π, π, π¦))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ ((π β β€ β§ π¦ β β€) β if(π¦ β€ π, π, π¦) β
(β€β₯βif(π¦ β€ π, π, π¦))) |
22 | 21, 14 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ ((π β β€ β§ π¦ β β€) β if(π¦ β€ π, π, π¦) β ((β€β₯βπ¦) β© π)) |
23 | 22 | elin2d 4163 |
. . . . . . . . 9
β’ ((π β β€ β§ π¦ β β€) β if(π¦ β€ π, π, π¦) β π) |
24 | | fnfvima 7187 |
. . . . . . . . 9
β’
((β€β₯ Fn β€ β§ π β β€ β§ if(π¦ β€ π, π, π¦) β π) β
(β€β₯βif(π¦ β€ π, π, π¦)) β (β€β₯ β
π)) |
25 | 16, 18, 23, 24 | mp3an12i 1466 |
. . . . . . . 8
β’ ((π β β€ β§ π¦ β β€) β
(β€β₯βif(π¦ β€ π, π, π¦)) β (β€β₯ β
π)) |
26 | 14, 25 | eqeltrd 2834 |
. . . . . . 7
β’ ((π β β€ β§ π¦ β β€) β
((β€β₯βπ¦) β© π) β (β€β₯ β
π)) |
27 | 26 | ralrimiva 3140 |
. . . . . 6
β’ (π β β€ β
βπ¦ β β€
((β€β₯βπ¦) β© π) β (β€β₯ β
π)) |
28 | | ineq1 4169 |
. . . . . . . . 9
β’ (π₯ =
(β€β₯βπ¦) β (π₯ β© π) = ((β€β₯βπ¦) β© π)) |
29 | 28 | eleq1d 2819 |
. . . . . . . 8
β’ (π₯ =
(β€β₯βπ¦) β ((π₯ β© π) β (β€β₯ β
π) β
((β€β₯βπ¦) β© π) β (β€β₯ β
π))) |
30 | 29 | ralrn 7042 |
. . . . . . 7
β’
(β€β₯ Fn β€ β (βπ₯ β ran β€β₯(π₯ β© π) β (β€β₯ β
π) β βπ¦ β β€
((β€β₯βπ¦) β© π) β (β€β₯ β
π))) |
31 | 16, 30 | ax-mp 5 |
. . . . . 6
β’
(βπ₯ β
ran β€β₯(π₯ β© π) β (β€β₯ β
π) β βπ¦ β β€
((β€β₯βπ¦) β© π) β (β€β₯ β
π)) |
32 | 27, 31 | sylibr 233 |
. . . . 5
β’ (π β β€ β
βπ₯ β ran
β€β₯(π₯
β© π) β
(β€β₯ β π)) |
33 | | eqid 2733 |
. . . . . 6
β’ (π₯ β ran
β€β₯ β¦ (π₯ β© π)) = (π₯ β ran β€β₯ β¦
(π₯ β© π)) |
34 | 33 | fmpt 7062 |
. . . . 5
β’
(βπ₯ β
ran β€β₯(π₯ β© π) β (β€β₯ β
π) β (π₯ β ran
β€β₯ β¦ (π₯ β© π)):ran
β€β₯βΆ(β€β₯ β π)) |
35 | 32, 34 | sylib 217 |
. . . 4
β’ (π β β€ β (π₯ β ran
β€β₯ β¦ (π₯ β© π)):ran
β€β₯βΆ(β€β₯ β π)) |
36 | 35 | frnd 6680 |
. . 3
β’ (π β β€ β ran
(π₯ β ran
β€β₯ β¦ (π₯ β© π)) β (β€β₯ β
π)) |
37 | 10, 36 | eqsstrid 3996 |
. 2
β’ (π β β€ β (ran
β€β₯ βΎt π) β (β€β₯ β
π)) |
38 | 7 | uztrn2 12790 |
. . . . . . . . 9
β’ ((π₯ β π β§ π¦ β (β€β₯βπ₯)) β π¦ β π) |
39 | 38 | ex 414 |
. . . . . . . 8
β’ (π₯ β π β (π¦ β (β€β₯βπ₯) β π¦ β π)) |
40 | 39 | ssrdv 3954 |
. . . . . . 7
β’ (π₯ β π β (β€β₯βπ₯) β π) |
41 | 40 | adantl 483 |
. . . . . 6
β’ ((π β β€ β§ π₯ β π) β (β€β₯βπ₯) β π) |
42 | | df-ss 3931 |
. . . . . 6
β’
((β€β₯βπ₯) β π β ((β€β₯βπ₯) β© π) = (β€β₯βπ₯)) |
43 | 41, 42 | sylib 217 |
. . . . 5
β’ ((π β β€ β§ π₯ β π) β
((β€β₯βπ₯) β© π) = (β€β₯βπ₯)) |
44 | 18 | sseli 3944 |
. . . . . . . 8
β’ (π₯ β π β π₯ β β€) |
45 | 44 | adantl 483 |
. . . . . . 7
β’ ((π β β€ β§ π₯ β π) β π₯ β β€) |
46 | | fnfvelrn 7035 |
. . . . . . 7
β’
((β€β₯ Fn β€ β§ π₯ β β€) β
(β€β₯βπ₯) β ran
β€β₯) |
47 | 16, 45, 46 | sylancr 588 |
. . . . . 6
β’ ((π β β€ β§ π₯ β π) β (β€β₯βπ₯) β ran
β€β₯) |
48 | | elrestr 17318 |
. . . . . 6
β’ ((ran
β€β₯ β V β§ π β V β§
(β€β₯βπ₯) β ran β€β₯) β
((β€β₯βπ₯) β© π) β (ran β€β₯
βΎt π)) |
49 | 6, 8, 47, 48 | mp3an12i 1466 |
. . . . 5
β’ ((π β β€ β§ π₯ β π) β
((β€β₯βπ₯) β© π) β (ran β€β₯
βΎt π)) |
50 | 43, 49 | eqeltrrd 2835 |
. . . 4
β’ ((π β β€ β§ π₯ β π) β (β€β₯βπ₯) β (ran
β€β₯ βΎt π)) |
51 | 50 | ralrimiva 3140 |
. . 3
β’ (π β β€ β
βπ₯ β π
(β€β₯βπ₯) β (ran β€β₯
βΎt π)) |
52 | | ffun 6675 |
. . . . 5
β’
(β€β₯:β€βΆπ« β€ β Fun
β€β₯) |
53 | 3, 52 | ax-mp 5 |
. . . 4
β’ Fun
β€β₯ |
54 | 3 | fdmi 6684 |
. . . . 5
β’ dom
β€β₯ = β€ |
55 | 18, 54 | sseqtrri 3985 |
. . . 4
β’ π β dom
β€β₯ |
56 | | funimass4 6911 |
. . . 4
β’ ((Fun
β€β₯ β§ π β dom β€β₯) β
((β€β₯ β π) β (ran β€β₯
βΎt π)
β βπ₯ β
π
(β€β₯βπ₯) β (ran β€β₯
βΎt π))) |
57 | 53, 55, 56 | mp2an 691 |
. . 3
β’
((β€β₯ β π) β (ran β€β₯
βΎt π)
β βπ₯ β
π
(β€β₯βπ₯) β (ran β€β₯
βΎt π)) |
58 | 51, 57 | sylibr 233 |
. 2
β’ (π β β€ β
(β€β₯ β π) β (ran β€β₯
βΎt π)) |
59 | 37, 58 | eqssd 3965 |
1
β’ (π β β€ β (ran
β€β₯ βΎt π) = (β€β₯ β π)) |