Step |
Hyp |
Ref |
Expression |
1 |
|
curry2.1 |
⊢ 𝐺 = ( 𝐹 ∘ ◡ ( 1st ↾ ( V × { 𝐶 } ) ) ) |
2 |
1
|
curry2 |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ) |
3 |
2
|
fveq1d |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 ‘ 𝐷 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) ) |
4 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) |
5 |
4
|
fvmptndm |
⊢ ( ¬ 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ∅ ) |
6 |
5
|
adantl |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ¬ 𝐷 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ∅ ) |
7 |
|
fndm |
⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → dom 𝐹 = ( 𝐴 × 𝐵 ) ) |
8 |
|
simpl |
⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → 𝐷 ∈ 𝐴 ) |
9 |
8
|
con3i |
⊢ ( ¬ 𝐷 ∈ 𝐴 → ¬ ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) |
10 |
|
ndmovg |
⊢ ( ( dom 𝐹 = ( 𝐴 × 𝐵 ) ∧ ¬ ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) → ( 𝐷 𝐹 𝐶 ) = ∅ ) |
11 |
7 9 10
|
syl2an |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ¬ 𝐷 ∈ 𝐴 ) → ( 𝐷 𝐹 𝐶 ) = ∅ ) |
12 |
6 11
|
eqtr4d |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ¬ 𝐷 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ( 𝐷 𝐹 𝐶 ) ) |
13 |
12
|
ex |
⊢ ( 𝐹 Fn ( 𝐴 × 𝐵 ) → ( ¬ 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ( 𝐷 𝐹 𝐶 ) ) ) |
14 |
13
|
adantr |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( ¬ 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ( 𝐷 𝐹 𝐶 ) ) ) |
15 |
|
oveq1 |
⊢ ( 𝑥 = 𝐷 → ( 𝑥 𝐹 𝐶 ) = ( 𝐷 𝐹 𝐶 ) ) |
16 |
|
ovex |
⊢ ( 𝐷 𝐹 𝐶 ) ∈ V |
17 |
15 4 16
|
fvmpt |
⊢ ( 𝐷 ∈ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ( 𝐷 𝐹 𝐶 ) ) |
18 |
14 17
|
pm2.61d2 |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) ‘ 𝐷 ) = ( 𝐷 𝐹 𝐶 ) ) |
19 |
3 18
|
eqtrd |
⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 ‘ 𝐷 ) = ( 𝐷 𝐹 𝐶 ) ) |