Step | Hyp | Ref
| Expression |
1 | | opex 4859 |
. . . . 5
⊢
〈𝐴, 𝐵〉 ∈ V |
2 | | brrestrict.3 |
. . . . 5
⊢ 𝐶 ∈ V |
3 | 1, 2 | brco 5214 |
. . . 4
⊢
(〈𝐴, 𝐵〉(Cap ∘
(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘
1st )))))𝐶
↔ ∃𝑥(〈𝐴, 𝐵〉(1st ⊗ (Cart ∘
(2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶)) |
4 | 1 | brtxp2 31158 |
. . . . . . 7
⊢
(〈𝐴, 𝐵〉(1st ⊗
(Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉1st 𝑎 ∧ 〈𝐴, 𝐵〉(Cart ∘ (2nd ⊗
(Range ∘ 1st )))𝑏)) |
5 | | 3anrot 1036 |
. . . . . . . . 9
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉1st 𝑎 ∧ 〈𝐴, 𝐵〉(Cart ∘ (2nd ⊗
(Range ∘ 1st )))𝑏) ↔ (〈𝐴, 𝐵〉1st 𝑎 ∧ 〈𝐴, 𝐵〉(Cart ∘ (2nd ⊗
(Range ∘ 1st )))𝑏 ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
6 | | brrestrict.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
7 | | brrestrict.2 |
. . . . . . . . . . 11
⊢ 𝐵 ∈ V |
8 | | vex 3176 |
. . . . . . . . . . 11
⊢ 𝑎 ∈ V |
9 | 6, 7, 8 | br1steq 30917 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐵〉1st 𝑎 ↔ 𝑎 = 𝐴) |
10 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑏 ∈ V |
11 | 1, 10 | brco 5214 |
. . . . . . . . . . 11
⊢
(〈𝐴, 𝐵〉(Cart ∘
(2nd ⊗ (Range ∘ 1st )))𝑏 ↔ ∃𝑥(〈𝐴, 𝐵〉(2nd ⊗ (Range
∘ 1st ))𝑥
∧ 𝑥Cart𝑏)) |
12 | 1 | brtxp2 31158 |
. . . . . . . . . . . . . . 15
⊢
(〈𝐴, 𝐵〉(2nd ⊗
(Range ∘ 1st ))𝑥 ↔ ∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉2nd 𝑎 ∧ 〈𝐴, 𝐵〉(Range ∘ 1st )𝑏)) |
13 | | 3anrot 1036 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉2nd 𝑎 ∧ 〈𝐴, 𝐵〉(Range ∘ 1st )𝑏) ↔ (〈𝐴, 𝐵〉2nd 𝑎 ∧ 〈𝐴, 𝐵〉(Range ∘ 1st )𝑏 ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
14 | 6, 7, 8 | br2ndeq 30918 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝐴, 𝐵〉2nd 𝑎 ↔ 𝑎 = 𝐵) |
15 | 1, 10 | brco 5214 |
. . . . . . . . . . . . . . . . . . 19
⊢
(〈𝐴, 𝐵〉(Range ∘
1st )𝑏 ↔
∃𝑥(〈𝐴, 𝐵〉1st 𝑥 ∧ 𝑥Range𝑏)) |
16 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑥 ∈ V |
17 | 6, 7, 16 | br1steq 30917 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝐴, 𝐵〉1st 𝑥 ↔ 𝑥 = 𝐴) |
18 | 17 | anbi1i 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((〈𝐴, 𝐵〉1st 𝑥 ∧ 𝑥Range𝑏) ↔ (𝑥 = 𝐴 ∧ 𝑥Range𝑏)) |
19 | 18 | exbii 1764 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥(〈𝐴, 𝐵〉1st 𝑥 ∧ 𝑥Range𝑏) ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏)) |
20 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝐴 → (𝑥Range𝑏 ↔ 𝐴Range𝑏)) |
21 | 6, 20 | ceqsexv 3215 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∃𝑥(𝑥 = 𝐴 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏) |
22 | 19, 21 | bitri 263 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑥(〈𝐴, 𝐵〉1st 𝑥 ∧ 𝑥Range𝑏) ↔ 𝐴Range𝑏) |
23 | 6, 10 | brrange 31211 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐴Range𝑏 ↔ 𝑏 = ran 𝐴) |
24 | 15, 22, 23 | 3bitri 285 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝐴, 𝐵〉(Range ∘
1st )𝑏 ↔
𝑏 = ran 𝐴) |
25 | | biid 250 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝑎, 𝑏〉) |
26 | 14, 24, 25 | 3anbi123i 1244 |
. . . . . . . . . . . . . . . . 17
⊢
((〈𝐴, 𝐵〉2nd 𝑎 ∧ 〈𝐴, 𝐵〉(Range ∘ 1st )𝑏 ∧ 𝑥 = 〈𝑎, 𝑏〉) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
27 | 13, 26 | bitri 263 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉2nd 𝑎 ∧ 〈𝐴, 𝐵〉(Range ∘ 1st )𝑏) ↔ (𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
28 | 27 | 2exbii 1765 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉2nd 𝑎 ∧ 〈𝐴, 𝐵〉(Range ∘ 1st )𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
29 | 6 | rnex 6992 |
. . . . . . . . . . . . . . . 16
⊢ ran 𝐴 ∈ V |
30 | | opeq1 4340 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝐵 → 〈𝑎, 𝑏〉 = 〈𝐵, 𝑏〉) |
31 | 30 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝐵 → (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝐵, 𝑏〉)) |
32 | | opeq2 4341 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = ran 𝐴 → 〈𝐵, 𝑏〉 = 〈𝐵, ran 𝐴〉) |
33 | 32 | eqeq2d 2620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = ran 𝐴 → (𝑥 = 〈𝐵, 𝑏〉 ↔ 𝑥 = 〈𝐵, ran 𝐴〉)) |
34 | 7, 29, 31, 33 | ceqsex2v 3218 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑎∃𝑏(𝑎 = 𝐵 ∧ 𝑏 = ran 𝐴 ∧ 𝑥 = 〈𝑎, 𝑏〉) ↔ 𝑥 = 〈𝐵, ran 𝐴〉) |
35 | 12, 28, 34 | 3bitri 285 |
. . . . . . . . . . . . . 14
⊢
(〈𝐴, 𝐵〉(2nd ⊗
(Range ∘ 1st ))𝑥 ↔ 𝑥 = 〈𝐵, ran 𝐴〉) |
36 | 35 | anbi1i 727 |
. . . . . . . . . . . . 13
⊢
((〈𝐴, 𝐵〉(2nd ⊗
(Range ∘ 1st ))𝑥 ∧ 𝑥Cart𝑏) ↔ (𝑥 = 〈𝐵, ran 𝐴〉 ∧ 𝑥Cart𝑏)) |
37 | 36 | exbii 1764 |
. . . . . . . . . . . 12
⊢
(∃𝑥(〈𝐴, 𝐵〉(2nd ⊗ (Range
∘ 1st ))𝑥
∧ 𝑥Cart𝑏) ↔ ∃𝑥(𝑥 = 〈𝐵, ran 𝐴〉 ∧ 𝑥Cart𝑏)) |
38 | | opex 4859 |
. . . . . . . . . . . . 13
⊢
〈𝐵, ran 𝐴〉 ∈ V |
39 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝐵, ran 𝐴〉 → (𝑥Cart𝑏 ↔ 〈𝐵, ran 𝐴〉Cart𝑏)) |
40 | 38, 39 | ceqsexv 3215 |
. . . . . . . . . . . 12
⊢
(∃𝑥(𝑥 = 〈𝐵, ran 𝐴〉 ∧ 𝑥Cart𝑏) ↔ 〈𝐵, ran 𝐴〉Cart𝑏) |
41 | 37, 40 | bitri 263 |
. . . . . . . . . . 11
⊢
(∃𝑥(〈𝐴, 𝐵〉(2nd ⊗ (Range
∘ 1st ))𝑥
∧ 𝑥Cart𝑏) ↔ 〈𝐵, ran 𝐴〉Cart𝑏) |
42 | 7, 29, 10 | brcart 31209 |
. . . . . . . . . . 11
⊢
(〈𝐵, ran 𝐴〉Cart𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴)) |
43 | 11, 41, 42 | 3bitri 285 |
. . . . . . . . . 10
⊢
(〈𝐴, 𝐵〉(Cart ∘
(2nd ⊗ (Range ∘ 1st )))𝑏 ↔ 𝑏 = (𝐵 × ran 𝐴)) |
44 | 9, 43, 25 | 3anbi123i 1244 |
. . . . . . . . 9
⊢
((〈𝐴, 𝐵〉1st 𝑎 ∧ 〈𝐴, 𝐵〉(Cart ∘ (2nd ⊗
(Range ∘ 1st )))𝑏 ∧ 𝑥 = 〈𝑎, 𝑏〉) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
45 | 5, 44 | bitri 263 |
. . . . . . . 8
⊢ ((𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉1st 𝑎 ∧ 〈𝐴, 𝐵〉(Cart ∘ (2nd ⊗
(Range ∘ 1st )))𝑏) ↔ (𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
46 | 45 | 2exbii 1765 |
. . . . . . 7
⊢
(∃𝑎∃𝑏(𝑥 = 〈𝑎, 𝑏〉 ∧ 〈𝐴, 𝐵〉1st 𝑎 ∧ 〈𝐴, 𝐵〉(Cart ∘ (2nd ⊗
(Range ∘ 1st )))𝑏) ↔ ∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = 〈𝑎, 𝑏〉)) |
47 | 7, 29 | xpex 6860 |
. . . . . . . 8
⊢ (𝐵 × ran 𝐴) ∈ V |
48 | | opeq1 4340 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
49 | 48 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (𝑥 = 〈𝑎, 𝑏〉 ↔ 𝑥 = 〈𝐴, 𝑏〉)) |
50 | | opeq2 4341 |
. . . . . . . . 9
⊢ (𝑏 = (𝐵 × ran 𝐴) → 〈𝐴, 𝑏〉 = 〈𝐴, (𝐵 × ran 𝐴)〉) |
51 | 50 | eqeq2d 2620 |
. . . . . . . 8
⊢ (𝑏 = (𝐵 × ran 𝐴) → (𝑥 = 〈𝐴, 𝑏〉 ↔ 𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉)) |
52 | 6, 47, 49, 51 | ceqsex2v 3218 |
. . . . . . 7
⊢
(∃𝑎∃𝑏(𝑎 = 𝐴 ∧ 𝑏 = (𝐵 × ran 𝐴) ∧ 𝑥 = 〈𝑎, 𝑏〉) ↔ 𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉) |
53 | 4, 46, 52 | 3bitri 285 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉(1st ⊗
(Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ↔ 𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉) |
54 | 53 | anbi1i 727 |
. . . . 5
⊢
((〈𝐴, 𝐵〉(1st ⊗
(Cart ∘ (2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ (𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉 ∧ 𝑥Cap𝐶)) |
55 | 54 | exbii 1764 |
. . . 4
⊢
(∃𝑥(〈𝐴, 𝐵〉(1st ⊗ (Cart ∘
(2nd ⊗ (Range ∘ 1st ))))𝑥 ∧ 𝑥Cap𝐶) ↔ ∃𝑥(𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉 ∧ 𝑥Cap𝐶)) |
56 | 3, 55 | bitri 263 |
. . 3
⊢
(〈𝐴, 𝐵〉(Cap ∘
(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘
1st )))))𝐶
↔ ∃𝑥(𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉 ∧ 𝑥Cap𝐶)) |
57 | | opex 4859 |
. . . 4
⊢
〈𝐴, (𝐵 × ran 𝐴)〉 ∈ V |
58 | | breq1 4586 |
. . . 4
⊢ (𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉 → (𝑥Cap𝐶 ↔ 〈𝐴, (𝐵 × ran 𝐴)〉Cap𝐶)) |
59 | 57, 58 | ceqsexv 3215 |
. . 3
⊢
(∃𝑥(𝑥 = 〈𝐴, (𝐵 × ran 𝐴)〉 ∧ 𝑥Cap𝐶) ↔ 〈𝐴, (𝐵 × ran 𝐴)〉Cap𝐶) |
60 | 6, 47, 2 | brcap 31217 |
. . 3
⊢
(〈𝐴, (𝐵 × ran 𝐴)〉Cap𝐶 ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴))) |
61 | 56, 59, 60 | 3bitri 285 |
. 2
⊢
(〈𝐴, 𝐵〉(Cap ∘
(1st ⊗ (Cart ∘ (2nd ⊗ (Range ∘
1st )))))𝐶
↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴))) |
62 | | df-restrict 31147 |
. . 3
⊢ Restrict
= (Cap ∘ (1st ⊗ (Cart ∘ (2nd ⊗
(Range ∘ 1st ))))) |
63 | 62 | breqi 4589 |
. 2
⊢
(〈𝐴, 𝐵〉Restrict𝐶 ↔ 〈𝐴, 𝐵〉(Cap ∘ (1st ⊗
(Cart ∘ (2nd ⊗ (Range ∘ 1st )))))𝐶) |
64 | | dfres3 30902 |
. . 3
⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴)) |
65 | 64 | eqeq2i 2622 |
. 2
⊢ (𝐶 = (𝐴 ↾ 𝐵) ↔ 𝐶 = (𝐴 ∩ (𝐵 × ran 𝐴))) |
66 | 61, 63, 65 | 3bitr4i 291 |
1
⊢
(〈𝐴, 𝐵〉Restrict𝐶 ↔ 𝐶 = (𝐴 ↾ 𝐵)) |