Step | Hyp | Ref
| Expression |
1 | | df-res 5563 |
. 2
⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) |
2 | | eleq1 2825 |
. . . . . . . . . 10
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ 𝐴 ↔ 〈𝑦, 𝑧〉 ∈ 𝐴)) |
3 | | vex 3412 |
. . . . . . . . . . . 12
⊢ 𝑧 ∈ V |
4 | 3 | biantru 533 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V)) |
5 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
6 | 5, 3 | opelrn 5812 |
. . . . . . . . . . . 12
⊢
(〈𝑦, 𝑧〉 ∈ 𝐴 → 𝑧 ∈ ran 𝐴) |
7 | 6 | biantrud 535 |
. . . . . . . . . . 11
⊢
(〈𝑦, 𝑧〉 ∈ 𝐴 → (𝑦 ∈ 𝐵 ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴))) |
8 | 4, 7 | bitr3id 288 |
. . . . . . . . . 10
⊢
(〈𝑦, 𝑧〉 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴))) |
9 | 2, 8 | syl6bi 256 |
. . . . . . . . 9
⊢ (𝑥 = 〈𝑦, 𝑧〉 → (𝑥 ∈ 𝐴 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴)))) |
10 | 9 | com12 32 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 → (𝑥 = 〈𝑦, 𝑧〉 → ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V) ↔ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴)))) |
11 | 10 | pm5.32d 580 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐴 → ((𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V)) ↔ (𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴)))) |
12 | 11 | 2exbidv 1932 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 → (∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V)) ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴)))) |
13 | | elxp 5574 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 × V) ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ V))) |
14 | | elxp 5574 |
. . . . . 6
⊢ (𝑥 ∈ (𝐵 × ran 𝐴) ↔ ∃𝑦∃𝑧(𝑥 = 〈𝑦, 𝑧〉 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ ran 𝐴))) |
15 | 12, 13, 14 | 3bitr4g 317 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 → (𝑥 ∈ (𝐵 × V) ↔ 𝑥 ∈ (𝐵 × ran 𝐴))) |
16 | 15 | pm5.32i 578 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 × V)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 × ran 𝐴))) |
17 | | elin 3882 |
. . . 4
⊢ (𝑥 ∈ (𝐴 ∩ (𝐵 × ran 𝐴)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 × ran 𝐴))) |
18 | 16, 17 | bitr4i 281 |
. . 3
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ (𝐵 × V)) ↔ 𝑥 ∈ (𝐴 ∩ (𝐵 × ran 𝐴))) |
19 | 18 | ineqri 4119 |
. 2
⊢ (𝐴 ∩ (𝐵 × V)) = (𝐴 ∩ (𝐵 × ran 𝐴)) |
20 | 1, 19 | eqtri 2765 |
1
⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴)) |