Step |
Hyp |
Ref |
Expression |
1 |
|
fndm |
⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 ) |
2 |
|
eleq2 |
⊢ ( 𝐴 = dom 𝐹 → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ∈ dom 𝐹 ) ) |
3 |
2
|
eqcoms |
⊢ ( dom 𝐹 = 𝐴 → ( 𝐵 ∈ 𝐴 ↔ 𝐵 ∈ dom 𝐹 ) ) |
4 |
3
|
biimpd |
⊢ ( dom 𝐹 = 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹 ) ) |
5 |
1 4
|
syl |
⊢ ( 𝐹 Fn 𝐴 → ( 𝐵 ∈ 𝐴 → 𝐵 ∈ dom 𝐹 ) ) |
6 |
5
|
imp |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → 𝐵 ∈ dom 𝐹 ) |
7 |
|
snssi |
⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 ) |
8 |
7
|
adantl |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → { 𝐵 } ⊆ 𝐴 ) |
9 |
|
fnssresb |
⊢ ( 𝐹 Fn 𝐴 → ( ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } ↔ { 𝐵 } ⊆ 𝐴 ) ) |
10 |
9
|
adantr |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } ↔ { 𝐵 } ⊆ 𝐴 ) ) |
11 |
8 10
|
mpbird |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } ) |
12 |
|
fnfun |
⊢ ( ( 𝐹 ↾ { 𝐵 } ) Fn { 𝐵 } → Fun ( 𝐹 ↾ { 𝐵 } ) ) |
13 |
11 12
|
syl |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → Fun ( 𝐹 ↾ { 𝐵 } ) ) |
14 |
|
df-dfat |
⊢ ( 𝐹 defAt 𝐵 ↔ ( 𝐵 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐵 } ) ) ) |
15 |
|
afvfundmfveq |
⊢ ( 𝐹 defAt 𝐵 → ( 𝐹 ''' 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) |
16 |
14 15
|
sylbir |
⊢ ( ( 𝐵 ∈ dom 𝐹 ∧ Fun ( 𝐹 ↾ { 𝐵 } ) ) → ( 𝐹 ''' 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) |
17 |
6 13 16
|
syl2anc |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( 𝐹 ''' 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) |
18 |
17
|
eqeq1d |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶 ↔ ( 𝐹 ‘ 𝐵 ) = 𝐶 ) ) |
19 |
|
fnbrfvb |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝐵 ) = 𝐶 ↔ 𝐵 𝐹 𝐶 ) ) |
20 |
18 19
|
bitrd |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴 ) → ( ( 𝐹 ''' 𝐵 ) = 𝐶 ↔ 𝐵 𝐹 𝐶 ) ) |