Step | Hyp | Ref
| Expression |
1 | | eqeq1 2742 |
. . . . . 6
⊢ (𝑧 = 𝐷 → (𝑧 = 𝐶 ↔ 𝐷 = 𝐶)) |
2 | 1 | anbi1d 631 |
. . . . 5
⊢ (𝑧 = 𝐷 → ((𝑧 = 𝐶 ∧ 𝑥𝑅𝑦) ↔ (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦))) |
3 | 2 | anbi2d 630 |
. . . 4
⊢ (𝑧 = 𝐷 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
4 | 3 | 2exbidv 1928 |
. . 3
⊢ (𝑧 = 𝐷 → (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
5 | | an12 644 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ 𝑅 ∧ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))) ↔ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ (𝑝 ∈ 𝑅 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)))) |
6 | | an12 644 |
. . . . . . . . . . . 12
⊢ ((𝑝 ∈ 𝑅 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶))) |
7 | | ancom 462 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 = 𝐶 ∧ 𝑝 ∈ 𝑅) ↔ (𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶)) |
8 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝑅 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅)) |
9 | | df-br 5105 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑅𝑦 ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑅) |
10 | 8, 9 | bitr4di 289 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (𝑝 ∈ 𝑅 ↔ 𝑥𝑅𝑦)) |
11 | 10 | anbi2d 630 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑧 = 𝐶 ∧ 𝑝 ∈ 𝑅) ↔ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))) |
12 | 7, 11 | bitr3id 285 |
. . . . . . . . . . . . 13
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶) ↔ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))) |
13 | 12 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
14 | 6, 13 | bitrid 283 |
. . . . . . . . . . 11
⊢ (𝑝 = ⟨𝑥, 𝑦⟩ → ((𝑝 ∈ 𝑅 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
15 | 14 | pm5.32i 576 |
. . . . . . . . . 10
⊢ ((𝑝 = ⟨𝑥, 𝑦⟩ ∧ (𝑝 ∈ 𝑅 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))) ↔ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
16 | 5, 15 | bitri 275 |
. . . . . . . . 9
⊢ ((𝑝 ∈ 𝑅 ∧ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))) ↔ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
17 | 16 | 2exbii 1852 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦(𝑝 ∈ 𝑅 ∧ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))) ↔ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
18 | | 19.42vv 1962 |
. . . . . . . 8
⊢
(∃𝑥∃𝑦(𝑝 ∈ 𝑅 ∧ (𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))) ↔ (𝑝 ∈ 𝑅 ∧ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)))) |
19 | 17, 18 | bitr3i 277 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))) ↔ (𝑝 ∈ 𝑅 ∧ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)))) |
20 | 19 | opabbii 5171 |
. . . . . 6
⊢
{⟨𝑝, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))} = {⟨𝑝, 𝑧⟩ ∣ (𝑝 ∈ 𝑅 ∧ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)))} |
21 | | dfoprab2 7408 |
. . . . . 6
⊢
{⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))} = {⟨𝑝, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦)))} |
22 | | rngop.1 |
. . . . . . . . 9
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |
23 | | df-mpo 7355 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} |
24 | | dfoprab2 7408 |
. . . . . . . . 9
⊢
{⟨⟨𝑥,
𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)} = {⟨𝑝, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))} |
25 | 22, 23, 24 | 3eqtri 2770 |
. . . . . . . 8
⊢ 𝐹 = {⟨𝑝, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))} |
26 | 25 | reseq1i 5930 |
. . . . . . 7
⊢ (𝐹 ↾ 𝑅) = ({⟨𝑝, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))} ↾ 𝑅) |
27 | | resopab 5985 |
. . . . . . 7
⊢
({⟨𝑝, 𝑧⟩ ∣ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶))} ↾ 𝑅) = {⟨𝑝, 𝑧⟩ ∣ (𝑝 ∈ 𝑅 ∧ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)))} |
28 | 26, 27 | eqtri 2766 |
. . . . . 6
⊢ (𝐹 ↾ 𝑅) = {⟨𝑝, 𝑧⟩ ∣ (𝑝 ∈ 𝑅 ∧ ∃𝑥∃𝑦(𝑝 = ⟨𝑥, 𝑦⟩ ∧ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑧 = 𝐶)))} |
29 | 20, 21, 28 | 3eqtr4ri 2777 |
. . . . 5
⊢ (𝐹 ↾ 𝑅) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))} |
30 | 29 | rneqi 5889 |
. . . 4
⊢ ran
(𝐹 ↾ 𝑅) = ran {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))} |
31 | | rnoprab 7453 |
. . . 4
⊢ ran
{⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))} = {𝑧 ∣ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))} |
32 | 30, 31 | eqtri 2766 |
. . 3
⊢ ran
(𝐹 ↾ 𝑅) = {𝑧 ∣ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑥𝑅𝑦))} |
33 | 4, 32 | elab2g 3631 |
. 2
⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran (𝐹 ↾ 𝑅) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦)))) |
34 | | r2ex 3191 |
. 2
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐵 (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦) ↔ ∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦))) |
35 | 33, 34 | bitr4di 289 |
1
⊢ (𝐷 ∈ 𝑉 → (𝐷 ∈ ran (𝐹 ↾ 𝑅) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝐷 = 𝐶 ∧ 𝑥𝑅𝑦))) |