Step |
Hyp |
Ref |
Expression |
1 |
|
2arymaptf.h |
⊢ 𝐻 = ( ℎ ∈ ( 2 -aryF 𝑋 ) ↦ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) ) |
2 |
|
fveq1 |
⊢ ( ℎ = 𝐹 → ( ℎ ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) = ( 𝐹 ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) |
3 |
2
|
mpoeq3dv |
⊢ ( ℎ = 𝐹 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝐹 ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) ) |
4 |
|
eqid |
⊢ ( 0 ..^ 2 ) = ( 0 ..^ 2 ) |
5 |
4
|
naryrcl |
⊢ ( ℎ ∈ ( 2 -aryF 𝑋 ) → ( 2 ∈ ℕ0 ∧ 𝑋 ∈ V ) ) |
6 |
|
mpoexga |
⊢ ( ( 𝑋 ∈ V ∧ 𝑋 ∈ V ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) ∈ V ) |
7 |
6
|
anidms |
⊢ ( 𝑋 ∈ V → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) ∈ V ) |
8 |
5 7
|
simpl2im |
⊢ ( ℎ ∈ ( 2 -aryF 𝑋 ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( ℎ ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) ∈ V ) |
9 |
3 1 8
|
fvmpt3 |
⊢ ( 𝐹 ∈ ( 2 -aryF 𝑋 ) → ( 𝐻 ‘ 𝐹 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝐹 ‘ { 〈 0 , 𝑥 〉 , 〈 1 , 𝑦 〉 } ) ) ) |