Step |
Hyp |
Ref |
Expression |
1 |
|
fvmptf.1 |
⊢ Ⅎ 𝑥 𝐴 |
2 |
|
fvmptf.2 |
⊢ Ⅎ 𝑥 𝐶 |
3 |
|
fvmptf.3 |
⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) |
4 |
|
fvmptf.4 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐷 ↦ 𝐵 ) |
5 |
4
|
dmmptss |
⊢ dom 𝐹 ⊆ 𝐷 |
6 |
5
|
sseli |
⊢ ( 𝐴 ∈ dom 𝐹 → 𝐴 ∈ 𝐷 ) |
7 |
|
eqid |
⊢ ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) |
8 |
4 7
|
fvmptex |
⊢ ( 𝐹 ‘ 𝐴 ) = ( ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) |
9 |
|
fvex |
⊢ ( I ‘ 𝐶 ) ∈ V |
10 |
|
nfcv |
⊢ Ⅎ 𝑥 I |
11 |
10 2
|
nffv |
⊢ Ⅎ 𝑥 ( I ‘ 𝐶 ) |
12 |
3
|
fveq2d |
⊢ ( 𝑥 = 𝐴 → ( I ‘ 𝐵 ) = ( I ‘ 𝐶 ) ) |
13 |
1 11 12 7
|
fvmptf |
⊢ ( ( 𝐴 ∈ 𝐷 ∧ ( I ‘ 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) = ( I ‘ 𝐶 ) ) |
14 |
9 13
|
mpan2 |
⊢ ( 𝐴 ∈ 𝐷 → ( ( 𝑥 ∈ 𝐷 ↦ ( I ‘ 𝐵 ) ) ‘ 𝐴 ) = ( I ‘ 𝐶 ) ) |
15 |
8 14
|
eqtrid |
⊢ ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ( I ‘ 𝐶 ) ) |
16 |
|
fvprc |
⊢ ( ¬ 𝐶 ∈ V → ( I ‘ 𝐶 ) = ∅ ) |
17 |
15 16
|
sylan9eq |
⊢ ( ( 𝐴 ∈ 𝐷 ∧ ¬ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐴 ) = ∅ ) |
18 |
17
|
expcom |
⊢ ( ¬ 𝐶 ∈ V → ( 𝐴 ∈ 𝐷 → ( 𝐹 ‘ 𝐴 ) = ∅ ) ) |
19 |
6 18
|
syl5 |
⊢ ( ¬ 𝐶 ∈ V → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ ) ) |
20 |
|
ndmfv |
⊢ ( ¬ 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) = ∅ ) |
21 |
19 20
|
pm2.61d1 |
⊢ ( ¬ 𝐶 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ ) |