Step |
Hyp |
Ref |
Expression |
0 |
|
cdsr |
⊢ ∥r |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
cvv |
⊢ V |
3 |
|
vx |
⊢ 𝑥 |
4 |
|
vy |
⊢ 𝑦 |
5 |
3
|
cv |
⊢ 𝑥 |
6 |
|
cbs |
⊢ Base |
7 |
1
|
cv |
⊢ 𝑤 |
8 |
7 6
|
cfv |
⊢ ( Base ‘ 𝑤 ) |
9 |
5 8
|
wcel |
⊢ 𝑥 ∈ ( Base ‘ 𝑤 ) |
10 |
|
vz |
⊢ 𝑧 |
11 |
10
|
cv |
⊢ 𝑧 |
12 |
|
cmulr |
⊢ .r |
13 |
7 12
|
cfv |
⊢ ( .r ‘ 𝑤 ) |
14 |
11 5 13
|
co |
⊢ ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) |
15 |
4
|
cv |
⊢ 𝑦 |
16 |
14 15
|
wceq |
⊢ ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 |
17 |
16 10 8
|
wrex |
⊢ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 |
18 |
9 17
|
wa |
⊢ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 ) |
19 |
18 3 4
|
copab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } |
20 |
1 2 19
|
cmpt |
⊢ ( 𝑤 ∈ V ↦ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } ) |
21 |
0 20
|
wceq |
⊢ ∥r = ( 𝑤 ∈ V ↦ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝑥 ∈ ( Base ‘ 𝑤 ) ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑤 ) ( 𝑧 ( .r ‘ 𝑤 ) 𝑥 ) = 𝑦 ) } ) |