Step | Hyp | Ref
| Expression |
1 | | inss2 4165 |
. . . . 5
⊢ (𝐶 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
2 | 1 | rnssi 5851 |
. . . 4
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐴 × 𝐵) |
3 | | rnxpss 6077 |
. . . 4
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
4 | 2, 3 | sstri 3931 |
. . 3
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ 𝐵 |
5 | | eqss 3937 |
. . 3
⊢ (ran
(𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ (ran (𝐶 ∩ (𝐴 × 𝐵)) ⊆ 𝐵 ∧ 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)))) |
6 | 4, 5 | mpbiran 706 |
. 2
⊢ (ran
(𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵))) |
7 | | inxpssres 5608 |
. . . . 5
⊢ (𝐶 ∩ (𝐴 × 𝐵)) ⊆ (𝐶 ↾ 𝐴) |
8 | 7 | rnssi 5851 |
. . . 4
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐶 ↾ 𝐴) |
9 | | sstr 3930 |
. . . 4
⊢ ((𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) ∧ ran (𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐶 ↾ 𝐴)) → 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
10 | 8, 9 | mpan2 688 |
. . 3
⊢ (𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) → 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
11 | | ssel 3915 |
. . . . . . 7
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → 𝑦 ∈ ran (𝐶 ↾ 𝐴))) |
12 | | vex 3435 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
13 | 12 | elrn2 5803 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝐶 ↾ 𝐴) ↔ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)) |
14 | 11, 13 | syl6ib 250 |
. . . . . 6
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
15 | 14 | ancld 551 |
. . . . 5
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)))) |
16 | 12 | elrn2 5803 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵))) |
17 | | opelinxp 5668 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ 𝐶)) |
18 | 12 | opelresi 5901 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐶)) |
19 | 18 | bianassc 640 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ 𝐶)) |
20 | 17, 19 | bitr4i 277 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
21 | 20 | exbii 1850 |
. . . . . 6
⊢
(∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥(𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
22 | | 19.42v 1957 |
. . . . . 6
⊢
(∃𝑥(𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
23 | 16, 21, 22 | 3bitri 297 |
. . . . 5
⊢ (𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
24 | 15, 23 | syl6ibr 251 |
. . . 4
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → 𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)))) |
25 | 24 | ssrdv 3928 |
. . 3
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵))) |
26 | 10, 25 | impbii 208 |
. 2
⊢ (𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
27 | 6, 26 | bitr2i 275 |
1
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |