Step |
Hyp |
Ref |
Expression |
1 |
|
rngop.1 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) |
2 |
|
eqeq1 |
⊢ ( 𝑧 = 𝐷 → ( 𝑧 = 𝐶 ↔ 𝐷 = 𝐶 ) ) |
3 |
2
|
anbi1d |
⊢ ( 𝑧 = 𝐷 → ( ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ↔ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) |
4 |
3
|
anbi2d |
⊢ ( 𝑧 = 𝐷 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
5 |
4
|
2exbidv |
⊢ ( 𝑧 = 𝐷 → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
6 |
|
an12 |
⊢ ( ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ) |
7 |
|
an12 |
⊢ ( ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ) ) |
8 |
|
ancom |
⊢ ( ( 𝑧 = 𝐶 ∧ 𝑝 ∈ 𝑅 ) ↔ ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ) |
9 |
|
eleq1 |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( 𝑝 ∈ 𝑅 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) ) |
10 |
|
df-br |
⊢ ( 𝑥 𝑅 𝑦 ↔ 〈 𝑥 , 𝑦 〉 ∈ 𝑅 ) |
11 |
9 10
|
bitr4di |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( 𝑝 ∈ 𝑅 ↔ 𝑥 𝑅 𝑦 ) ) |
12 |
11
|
anbi2d |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ( 𝑧 = 𝐶 ∧ 𝑝 ∈ 𝑅 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) |
13 |
8 12
|
bitr3id |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ↔ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) |
14 |
13
|
anbi2d |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝑅 ∧ 𝑧 = 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
15 |
7 14
|
bitrid |
⊢ ( 𝑝 = 〈 𝑥 , 𝑦 〉 → ( ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
16 |
15
|
pm5.32i |
⊢ ( ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝑝 ∈ 𝑅 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
17 |
6 16
|
bitri |
⊢ ( ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
18 |
17
|
2exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
19 |
|
19.42vv |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 ∈ 𝑅 ∧ ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ↔ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ) |
20 |
18 19
|
bitr3i |
⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ↔ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) ) |
21 |
20
|
opabbii |
⊢ { 〈 𝑝 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) } = { 〈 𝑝 , 𝑧 〉 ∣ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) } |
22 |
|
dfoprab2 |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } = { 〈 𝑝 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) } |
23 |
|
df-mpo |
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } |
24 |
|
dfoprab2 |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { 〈 𝑝 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } |
25 |
1 23 24
|
3eqtri |
⊢ 𝐹 = { 〈 𝑝 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } |
26 |
25
|
reseq1i |
⊢ ( 𝐹 ↾ 𝑅 ) = ( { 〈 𝑝 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } ↾ 𝑅 ) |
27 |
|
resopab |
⊢ ( { 〈 𝑝 , 𝑧 〉 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } ↾ 𝑅 ) = { 〈 𝑝 , 𝑧 〉 ∣ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) } |
28 |
26 27
|
eqtri |
⊢ ( 𝐹 ↾ 𝑅 ) = { 〈 𝑝 , 𝑧 〉 ∣ ( 𝑝 ∈ 𝑅 ∧ ∃ 𝑥 ∃ 𝑦 ( 𝑝 = 〈 𝑥 , 𝑦 〉 ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) ) } |
29 |
21 22 28
|
3eqtr4ri |
⊢ ( 𝐹 ↾ 𝑅 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } |
30 |
29
|
rneqi |
⊢ ran ( 𝐹 ↾ 𝑅 ) = ran { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } |
31 |
|
rnoprab |
⊢ ran { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } |
32 |
30 31
|
eqtri |
⊢ ran ( 𝐹 ↾ 𝑅 ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) } |
33 |
5 32
|
elab2g |
⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran ( 𝐹 ↾ 𝑅 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) ) |
34 |
|
r2ex |
⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) |
35 |
33 34
|
bitr4di |
⊢ ( 𝐷 ∈ 𝑉 → ( 𝐷 ∈ ran ( 𝐹 ↾ 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ( 𝐷 = 𝐶 ∧ 𝑥 𝑅 𝑦 ) ) ) |