| Step | Hyp | Ref
| Expression |
| 1 | | inss2 4238 |
. . . . 5
⊢ (𝐶 ∩ (𝐴 × 𝐵)) ⊆ (𝐴 × 𝐵) |
| 2 | 1 | rnssi 5951 |
. . . 4
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐴 × 𝐵) |
| 3 | | rnxpss 6192 |
. . . 4
⊢ ran
(𝐴 × 𝐵) ⊆ 𝐵 |
| 4 | 2, 3 | sstri 3993 |
. . 3
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ 𝐵 |
| 5 | | eqss 3999 |
. . 3
⊢ (ran
(𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ (ran (𝐶 ∩ (𝐴 × 𝐵)) ⊆ 𝐵 ∧ 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)))) |
| 6 | 4, 5 | mpbiran 709 |
. 2
⊢ (ran
(𝐶 ∩ (𝐴 × 𝐵)) = 𝐵 ↔ 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵))) |
| 7 | | inxpssres 5702 |
. . . . 5
⊢ (𝐶 ∩ (𝐴 × 𝐵)) ⊆ (𝐶 ↾ 𝐴) |
| 8 | 7 | rnssi 5951 |
. . . 4
⊢ ran
(𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐶 ↾ 𝐴) |
| 9 | | sstr 3992 |
. . . 4
⊢ ((𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) ∧ ran (𝐶 ∩ (𝐴 × 𝐵)) ⊆ ran (𝐶 ↾ 𝐴)) → 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
| 10 | 8, 9 | mpan2 691 |
. . 3
⊢ (𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) → 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
| 11 | | ssel 3977 |
. . . . . . 7
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → 𝑦 ∈ ran (𝐶 ↾ 𝐴))) |
| 12 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 13 | 12 | elrn2 5903 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝐶 ↾ 𝐴) ↔ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)) |
| 14 | 11, 13 | imbitrdi 251 |
. . . . . 6
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
| 15 | 14 | ancld 550 |
. . . . 5
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → (𝑦 ∈ 𝐵 ∧ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)))) |
| 16 | 12 | elrn2 5903 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵))) |
| 17 | | opelinxp 5765 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ 𝐶)) |
| 18 | 12 | opelresi 6005 |
. . . . . . . . 9
⊢
(〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴) ↔ (𝑥 ∈ 𝐴 ∧ 〈𝑥, 𝑦〉 ∈ 𝐶)) |
| 19 | 18 | bianassc 643 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 〈𝑥, 𝑦〉 ∈ 𝐶)) |
| 20 | 17, 19 | bitr4i 278 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
| 21 | 20 | exbii 1848 |
. . . . . 6
⊢
(∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ∩ (𝐴 × 𝐵)) ↔ ∃𝑥(𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
| 22 | | 19.42v 1953 |
. . . . . 6
⊢
(∃𝑥(𝑦 ∈ 𝐵 ∧ 〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴)) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
| 23 | 16, 21, 22 | 3bitri 297 |
. . . . 5
⊢ (𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ (𝑦 ∈ 𝐵 ∧ ∃𝑥〈𝑥, 𝑦〉 ∈ (𝐶 ↾ 𝐴))) |
| 24 | 15, 23 | imbitrrdi 252 |
. . . 4
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → (𝑦 ∈ 𝐵 → 𝑦 ∈ ran (𝐶 ∩ (𝐴 × 𝐵)))) |
| 25 | 24 | ssrdv 3989 |
. . 3
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) → 𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵))) |
| 26 | 10, 25 | impbii 209 |
. 2
⊢ (𝐵 ⊆ ran (𝐶 ∩ (𝐴 × 𝐵)) ↔ 𝐵 ⊆ ran (𝐶 ↾ 𝐴)) |
| 27 | 6, 26 | bitr2i 276 |
1
⊢ (𝐵 ⊆ ran (𝐶 ↾ 𝐴) ↔ ran (𝐶 ∩ (𝐴 × 𝐵)) = 𝐵) |