Step |
Hyp |
Ref |
Expression |
1 |
|
fo2nd |
⊢ 2nd : V –onto→ V |
2 |
|
fofn |
⊢ ( 2nd : V –onto→ V → 2nd Fn V ) |
3 |
1 2
|
ax-mp |
⊢ 2nd Fn V |
4 |
|
dffn5 |
⊢ ( 2nd Fn V ↔ 2nd = ( 𝑤 ∈ V ↦ ( 2nd ‘ 𝑤 ) ) ) |
5 |
3 4
|
mpbi |
⊢ 2nd = ( 𝑤 ∈ V ↦ ( 2nd ‘ 𝑤 ) ) |
6 |
|
mptv |
⊢ ( 𝑤 ∈ V ↦ ( 2nd ‘ 𝑤 ) ) = { 〈 𝑤 , 𝑧 〉 ∣ 𝑧 = ( 2nd ‘ 𝑤 ) } |
7 |
5 6
|
eqtri |
⊢ 2nd = { 〈 𝑤 , 𝑧 〉 ∣ 𝑧 = ( 2nd ‘ 𝑤 ) } |
8 |
7
|
reseq1i |
⊢ ( 2nd ↾ ( V × V ) ) = ( { 〈 𝑤 , 𝑧 〉 ∣ 𝑧 = ( 2nd ‘ 𝑤 ) } ↾ ( V × V ) ) |
9 |
|
resopab |
⊢ ( { 〈 𝑤 , 𝑧 〉 ∣ 𝑧 = ( 2nd ‘ 𝑤 ) } ↾ ( V × V ) ) = { 〈 𝑤 , 𝑧 〉 ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 = ( 2nd ‘ 𝑤 ) ) } |
10 |
|
vex |
⊢ 𝑥 ∈ V |
11 |
|
vex |
⊢ 𝑦 ∈ V |
12 |
10 11
|
op2ndd |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → ( 2nd ‘ 𝑤 ) = 𝑦 ) |
13 |
12
|
eqeq2d |
⊢ ( 𝑤 = 〈 𝑥 , 𝑦 〉 → ( 𝑧 = ( 2nd ‘ 𝑤 ) ↔ 𝑧 = 𝑦 ) ) |
14 |
13
|
dfoprab3 |
⊢ { 〈 𝑤 , 𝑧 〉 ∣ ( 𝑤 ∈ ( V × V ) ∧ 𝑧 = ( 2nd ‘ 𝑤 ) ) } = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝑧 = 𝑦 } |
15 |
8 9 14
|
3eqtrri |
⊢ { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ 𝑧 = 𝑦 } = ( 2nd ↾ ( V × V ) ) |