Step | Hyp | Ref
| Expression |
1 | | opex 5422 |
. . . . 5
β’
β¨π΄, π΅β© β V |
2 | | brrestrict.3 |
. . . . 5
β’ πΆ β V |
3 | 1, 2 | brco 5827 |
. . . 4
β’
(β¨π΄, π΅β©(Cap β
(1st β (Cart β (2nd β (Range β
1st )))))πΆ
β βπ₯(β¨π΄, π΅β©(1st β (Cart β
(2nd β (Range β 1st ))))π₯ β§ π₯CapπΆ)) |
4 | 1 | brtxp2 34512 |
. . . . . . 7
β’
(β¨π΄, π΅β©(1st β
(Cart β (2nd β (Range β 1st ))))π₯ β βπβπ(π₯ = β¨π, πβ© β§ β¨π΄, π΅β©1st π β§ β¨π΄, π΅β©(Cart β (2nd β
(Range β 1st )))π)) |
5 | | 3anrot 1101 |
. . . . . . . . 9
β’ ((π₯ = β¨π, πβ© β§ β¨π΄, π΅β©1st π β§ β¨π΄, π΅β©(Cart β (2nd β
(Range β 1st )))π) β (β¨π΄, π΅β©1st π β§ β¨π΄, π΅β©(Cart β (2nd β
(Range β 1st )))π β§ π₯ = β¨π, πβ©)) |
6 | | brrestrict.1 |
. . . . . . . . . . 11
β’ π΄ β V |
7 | | brrestrict.2 |
. . . . . . . . . . 11
β’ π΅ β V |
8 | 6, 7 | br1steq 34401 |
. . . . . . . . . 10
β’
(β¨π΄, π΅β©1st π β π = π΄) |
9 | | vex 3448 |
. . . . . . . . . . . 12
β’ π β V |
10 | 1, 9 | brco 5827 |
. . . . . . . . . . 11
β’
(β¨π΄, π΅β©(Cart β
(2nd β (Range β 1st )))π β βπ₯(β¨π΄, π΅β©(2nd β (Range
β 1st ))π₯
β§ π₯Cartπ)) |
11 | 1 | brtxp2 34512 |
. . . . . . . . . . . . . . 15
β’
(β¨π΄, π΅β©(2nd β
(Range β 1st ))π₯ β βπβπ(π₯ = β¨π, πβ© β§ β¨π΄, π΅β©2nd π β§ β¨π΄, π΅β©(Range β 1st )π)) |
12 | | 3anrot 1101 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ = β¨π, πβ© β§ β¨π΄, π΅β©2nd π β§ β¨π΄, π΅β©(Range β 1st )π) β (β¨π΄, π΅β©2nd π β§ β¨π΄, π΅β©(Range β 1st )π β§ π₯ = β¨π, πβ©)) |
13 | 6, 7 | br2ndeq 34402 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π΄, π΅β©2nd π β π = π΅) |
14 | 1, 9 | brco 5827 |
. . . . . . . . . . . . . . . . . . 19
β’
(β¨π΄, π΅β©(Range β
1st )π β
βπ₯(β¨π΄, π΅β©1st π₯ β§ π₯Rangeπ)) |
15 | 6, 7 | br1steq 34401 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(β¨π΄, π΅β©1st π₯ β π₯ = π΄) |
16 | 15 | anbi1i 625 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((β¨π΄, π΅β©1st π₯ β§ π₯Rangeπ) β (π₯ = π΄ β§ π₯Rangeπ)) |
17 | 16 | exbii 1851 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ₯(β¨π΄, π΅β©1st π₯ β§ π₯Rangeπ) β βπ₯(π₯ = π΄ β§ π₯Rangeπ)) |
18 | | breq1 5109 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π΄ β (π₯Rangeπ β π΄Rangeπ)) |
19 | 6, 18 | ceqsexv 3493 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ₯(π₯ = π΄ β§ π₯Rangeπ) β π΄Rangeπ) |
20 | 17, 19 | bitri 275 |
. . . . . . . . . . . . . . . . . . 19
β’
(βπ₯(β¨π΄, π΅β©1st π₯ β§ π₯Rangeπ) β π΄Rangeπ) |
21 | 6, 9 | brrange 34565 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄Rangeπ β π = ran π΄) |
22 | 14, 20, 21 | 3bitri 297 |
. . . . . . . . . . . . . . . . . 18
β’
(β¨π΄, π΅β©(Range β
1st )π β
π = ran π΄) |
23 | | biid 261 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = β¨π, πβ© β π₯ = β¨π, πβ©) |
24 | 13, 22, 23 | 3anbi123i 1156 |
. . . . . . . . . . . . . . . . 17
β’
((β¨π΄, π΅β©2nd π β§ β¨π΄, π΅β©(Range β 1st )π β§ π₯ = β¨π, πβ©) β (π = π΅ β§ π = ran π΄ β§ π₯ = β¨π, πβ©)) |
25 | 12, 24 | bitri 275 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ = β¨π, πβ© β§ β¨π΄, π΅β©2nd π β§ β¨π΄, π΅β©(Range β 1st )π) β (π = π΅ β§ π = ran π΄ β§ π₯ = β¨π, πβ©)) |
26 | 25 | 2exbii 1852 |
. . . . . . . . . . . . . . 15
β’
(βπβπ(π₯ = β¨π, πβ© β§ β¨π΄, π΅β©2nd π β§ β¨π΄, π΅β©(Range β 1st )π) β βπβπ(π = π΅ β§ π = ran π΄ β§ π₯ = β¨π, πβ©)) |
27 | 6 | rnex 7850 |
. . . . . . . . . . . . . . . 16
β’ ran π΄ β V |
28 | | opeq1 4831 |
. . . . . . . . . . . . . . . . 17
β’ (π = π΅ β β¨π, πβ© = β¨π΅, πβ©) |
29 | 28 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π = π΅ β (π₯ = β¨π, πβ© β π₯ = β¨π΅, πβ©)) |
30 | | opeq2 4832 |
. . . . . . . . . . . . . . . . 17
β’ (π = ran π΄ β β¨π΅, πβ© = β¨π΅, ran π΄β©) |
31 | 30 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ (π = ran π΄ β (π₯ = β¨π΅, πβ© β π₯ = β¨π΅, ran π΄β©)) |
32 | 7, 27, 29, 31 | ceqsex2v 3498 |
. . . . . . . . . . . . . . 15
β’
(βπβπ(π = π΅ β§ π = ran π΄ β§ π₯ = β¨π, πβ©) β π₯ = β¨π΅, ran π΄β©) |
33 | 11, 26, 32 | 3bitri 297 |
. . . . . . . . . . . . . 14
β’
(β¨π΄, π΅β©(2nd β
(Range β 1st ))π₯ β π₯ = β¨π΅, ran π΄β©) |
34 | 33 | anbi1i 625 |
. . . . . . . . . . . . 13
β’
((β¨π΄, π΅β©(2nd β
(Range β 1st ))π₯ β§ π₯Cartπ) β (π₯ = β¨π΅, ran π΄β© β§ π₯Cartπ)) |
35 | 34 | exbii 1851 |
. . . . . . . . . . . 12
β’
(βπ₯(β¨π΄, π΅β©(2nd β (Range
β 1st ))π₯
β§ π₯Cartπ) β βπ₯(π₯ = β¨π΅, ran π΄β© β§ π₯Cartπ)) |
36 | | opex 5422 |
. . . . . . . . . . . . 13
β’
β¨π΅, ran π΄β© β V |
37 | | breq1 5109 |
. . . . . . . . . . . . 13
β’ (π₯ = β¨π΅, ran π΄β© β (π₯Cartπ β β¨π΅, ran π΄β©Cartπ)) |
38 | 36, 37 | ceqsexv 3493 |
. . . . . . . . . . . 12
β’
(βπ₯(π₯ = β¨π΅, ran π΄β© β§ π₯Cartπ) β β¨π΅, ran π΄β©Cartπ) |
39 | 35, 38 | bitri 275 |
. . . . . . . . . . 11
β’
(βπ₯(β¨π΄, π΅β©(2nd β (Range
β 1st ))π₯
β§ π₯Cartπ) β β¨π΅, ran π΄β©Cartπ) |
40 | 7, 27, 9 | brcart 34563 |
. . . . . . . . . . 11
β’
(β¨π΅, ran π΄β©Cartπ β π = (π΅ Γ ran π΄)) |
41 | 10, 39, 40 | 3bitri 297 |
. . . . . . . . . 10
β’
(β¨π΄, π΅β©(Cart β
(2nd β (Range β 1st )))π β π = (π΅ Γ ran π΄)) |
42 | 8, 41, 23 | 3anbi123i 1156 |
. . . . . . . . 9
β’
((β¨π΄, π΅β©1st π β§ β¨π΄, π΅β©(Cart β (2nd β
(Range β 1st )))π β§ π₯ = β¨π, πβ©) β (π = π΄ β§ π = (π΅ Γ ran π΄) β§ π₯ = β¨π, πβ©)) |
43 | 5, 42 | bitri 275 |
. . . . . . . 8
β’ ((π₯ = β¨π, πβ© β§ β¨π΄, π΅β©1st π β§ β¨π΄, π΅β©(Cart β (2nd β
(Range β 1st )))π) β (π = π΄ β§ π = (π΅ Γ ran π΄) β§ π₯ = β¨π, πβ©)) |
44 | 43 | 2exbii 1852 |
. . . . . . 7
β’
(βπβπ(π₯ = β¨π, πβ© β§ β¨π΄, π΅β©1st π β§ β¨π΄, π΅β©(Cart β (2nd β
(Range β 1st )))π) β βπβπ(π = π΄ β§ π = (π΅ Γ ran π΄) β§ π₯ = β¨π, πβ©)) |
45 | 7, 27 | xpex 7688 |
. . . . . . . 8
β’ (π΅ Γ ran π΄) β V |
46 | | opeq1 4831 |
. . . . . . . . 9
β’ (π = π΄ β β¨π, πβ© = β¨π΄, πβ©) |
47 | 46 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = π΄ β (π₯ = β¨π, πβ© β π₯ = β¨π΄, πβ©)) |
48 | | opeq2 4832 |
. . . . . . . . 9
β’ (π = (π΅ Γ ran π΄) β β¨π΄, πβ© = β¨π΄, (π΅ Γ ran π΄)β©) |
49 | 48 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = (π΅ Γ ran π΄) β (π₯ = β¨π΄, πβ© β π₯ = β¨π΄, (π΅ Γ ran π΄)β©)) |
50 | 6, 45, 47, 49 | ceqsex2v 3498 |
. . . . . . 7
β’
(βπβπ(π = π΄ β§ π = (π΅ Γ ran π΄) β§ π₯ = β¨π, πβ©) β π₯ = β¨π΄, (π΅ Γ ran π΄)β©) |
51 | 4, 44, 50 | 3bitri 297 |
. . . . . 6
β’
(β¨π΄, π΅β©(1st β
(Cart β (2nd β (Range β 1st ))))π₯ β π₯ = β¨π΄, (π΅ Γ ran π΄)β©) |
52 | 51 | anbi1i 625 |
. . . . 5
β’
((β¨π΄, π΅β©(1st β
(Cart β (2nd β (Range β 1st ))))π₯ β§ π₯CapπΆ) β (π₯ = β¨π΄, (π΅ Γ ran π΄)β© β§ π₯CapπΆ)) |
53 | 52 | exbii 1851 |
. . . 4
β’
(βπ₯(β¨π΄, π΅β©(1st β (Cart β
(2nd β (Range β 1st ))))π₯ β§ π₯CapπΆ) β βπ₯(π₯ = β¨π΄, (π΅ Γ ran π΄)β© β§ π₯CapπΆ)) |
54 | 3, 53 | bitri 275 |
. . 3
β’
(β¨π΄, π΅β©(Cap β
(1st β (Cart β (2nd β (Range β
1st )))))πΆ
β βπ₯(π₯ = β¨π΄, (π΅ Γ ran π΄)β© β§ π₯CapπΆ)) |
55 | | opex 5422 |
. . . 4
β’
β¨π΄, (π΅ Γ ran π΄)β© β V |
56 | | breq1 5109 |
. . . 4
β’ (π₯ = β¨π΄, (π΅ Γ ran π΄)β© β (π₯CapπΆ β β¨π΄, (π΅ Γ ran π΄)β©CapπΆ)) |
57 | 55, 56 | ceqsexv 3493 |
. . 3
β’
(βπ₯(π₯ = β¨π΄, (π΅ Γ ran π΄)β© β§ π₯CapπΆ) β β¨π΄, (π΅ Γ ran π΄)β©CapπΆ) |
58 | 6, 45, 2 | brcap 34571 |
. . 3
β’
(β¨π΄, (π΅ Γ ran π΄)β©CapπΆ β πΆ = (π΄ β© (π΅ Γ ran π΄))) |
59 | 54, 57, 58 | 3bitri 297 |
. 2
β’
(β¨π΄, π΅β©(Cap β
(1st β (Cart β (2nd β (Range β
1st )))))πΆ
β πΆ = (π΄ β© (π΅ Γ ran π΄))) |
60 | | df-restrict 34502 |
. . 3
β’ Restrict
= (Cap β (1st β (Cart β (2nd β
(Range β 1st ))))) |
61 | 60 | breqi 5112 |
. 2
β’
(β¨π΄, π΅β©RestrictπΆ β β¨π΄, π΅β©(Cap β (1st β
(Cart β (2nd β (Range β 1st )))))πΆ) |
62 | | dfres3 5943 |
. . 3
β’ (π΄ βΎ π΅) = (π΄ β© (π΅ Γ ran π΄)) |
63 | 62 | eqeq2i 2746 |
. 2
β’ (πΆ = (π΄ βΎ π΅) β πΆ = (π΄ β© (π΅ Γ ran π΄))) |
64 | 59, 61, 63 | 3bitr4i 303 |
1
β’
(β¨π΄, π΅β©RestrictπΆ β πΆ = (π΄ βΎ π΅)) |