Step | Hyp | Ref
| Expression |
1 | | inss2 4193 |
. . . . 5
⊢ (𝐶 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
2 | 1 | rnssi 5899 |
. . . 4
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐴 × 𝐵) |
3 | | rnxpss 6128 |
. . . 4
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
4 | 2, 3 | sstri 3957 |
. . 3
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ 𝐵 |
5 | | eqss 3963 |
. . 3
⊢ (ran
(𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ (ran (𝐶 ∩ (𝐴 × 𝐵)) ⊆ 𝐵 ∧ 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)))) |
6 | 4, 5 | mpbiran 708 |
. 2
⊢ (ran
(𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵))) |
7 | | inxpssres 5654 |
. . . . 5
⊢ (𝐶 ∩ (𝐴 × 𝐵)) ⊆ (𝐶 ↾ 𝐴) |
8 | 7 | rnssi 5899 |
. . . 4
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐶 ↾ 𝐴) |
9 | | sstr 3956 |
. . . 4
⊢ ((𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) ∧ ran (𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐶 ↾ 𝐴)) → 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
10 | 8, 9 | mpan2 690 |
. . 3
⊢ (𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) → 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
11 | | ssel 3941 |
. . . . . . 7
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → 𝑦 ∈ ran (𝐶 ↾ 𝐴))) |
12 | | vex 3451 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
13 | 12 | elrn2 5852 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝐶 ↾ 𝐴) ↔ ∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴)) |
14 | 11, 13 | syl6ib 251 |
. . . . . 6
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴))) |
15 | 14 | ancld 552 |
. . . . 5
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ ∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴)))) |
16 | 12 | elrn2 5852 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ∩ (𝐴 × 𝐵))) |
17 | | opelinxp 5715 |
. . . . . . . 8
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐶)) |
18 | 12 | opelresi 5949 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐶)) |
19 | 18 | bianassc 642 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐶)) |
20 | 17, 19 | bitr4i 278 |
. . . . . . 7
⊢
(⟨𝑥, 𝑦⟩ ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴))) |
21 | 20 | exbii 1851 |
. . . . . 6
⊢
(∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥(𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴))) |
22 | | 19.42v 1958 |
. . . . . 6
⊢
(∃𝑥(𝑦 ∈ 𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴)) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴))) |
23 | 16, 21, 22 | 3bitri 297 |
. . . . 5
⊢ (𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥⟨𝑥, 𝑦⟩ ∈ (𝐶 ↾ 𝐴))) |
24 | 15, 23 | syl6ibr 252 |
. . . 4
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → 𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)))) |
25 | 24 | ssrdv 3954 |
. . 3
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵))) |
26 | 10, 25 | impbii 208 |
. 2
⊢ (𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
27 | 6, 26 | bitr2i 276 |
1
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |