Proof of Theorem afvres
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elin 3966 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝐵 ∩ dom 𝐹) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹)) | 
| 2 | 1 | biimpri 228 | . . . . . . . 8
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹) → 𝐴 ∈ (𝐵 ∩ dom 𝐹)) | 
| 3 |  | dmres 6029 | . . . . . . . 8
⊢ dom
(𝐹 ↾ 𝐵) = (𝐵 ∩ dom 𝐹) | 
| 4 | 2, 3 | eleqtrrdi 2851 | . . . . . . 7
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹) → 𝐴 ∈ dom (𝐹 ↾ 𝐵)) | 
| 5 | 4 | ex 412 | . . . . . 6
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ dom 𝐹 → 𝐴 ∈ dom (𝐹 ↾ 𝐵))) | 
| 6 |  | snssi 4807 | . . . . . . . . . 10
⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵) | 
| 7 | 6 | resabs1d 6025 | . . . . . . . . 9
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵) ↾ {𝐴}) = (𝐹 ↾ {𝐴})) | 
| 8 | 7 | eqcomd 2742 | . . . . . . . 8
⊢ (𝐴 ∈ 𝐵 → (𝐹 ↾ {𝐴}) = ((𝐹 ↾ 𝐵) ↾ {𝐴})) | 
| 9 | 8 | funeqd 6587 | . . . . . . 7
⊢ (𝐴 ∈ 𝐵 → (Fun (𝐹 ↾ {𝐴}) ↔ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))) | 
| 10 | 9 | biimpd 229 | . . . . . 6
⊢ (𝐴 ∈ 𝐵 → (Fun (𝐹 ↾ {𝐴}) → Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))) | 
| 11 | 5, 10 | anim12d 609 | . . . . 5
⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})))) | 
| 12 | 11 | impcom 407 | . . . 4
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))) | 
| 13 |  | df-dfat 47136 | . . . . 5
⊢ ((𝐹 ↾ 𝐵) defAt 𝐴 ↔ (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))) | 
| 14 |  | afvfundmfveq 47155 | . . . . 5
⊢ ((𝐹 ↾ 𝐵) defAt 𝐴 → ((𝐹 ↾ 𝐵)'''𝐴) = ((𝐹 ↾ 𝐵)‘𝐴)) | 
| 15 | 13, 14 | sylbir 235 | . . . 4
⊢ ((𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})) → ((𝐹 ↾ 𝐵)'''𝐴) = ((𝐹 ↾ 𝐵)‘𝐴)) | 
| 16 | 12, 15 | syl 17 | . . 3
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)'''𝐴) = ((𝐹 ↾ 𝐵)‘𝐴)) | 
| 17 |  | fvres 6924 | . . . 4
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴)) | 
| 18 | 17 | adantl 481 | . . 3
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴)) | 
| 19 |  | df-dfat 47136 | . . . . . 6
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) | 
| 20 |  | afvfundmfveq 47155 | . . . . . 6
⊢ (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹‘𝐴)) | 
| 21 | 19, 20 | sylbir 235 | . . . . 5
⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹'''𝐴) = (𝐹‘𝐴)) | 
| 22 | 21 | eqcomd 2742 | . . . 4
⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹‘𝐴) = (𝐹'''𝐴)) | 
| 23 | 22 | adantr 480 | . . 3
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) = (𝐹'''𝐴)) | 
| 24 | 16, 18, 23 | 3eqtrd 2780 | . 2
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) | 
| 25 |  | pm3.4 809 | . . . . . . . . . 10
⊢ ((𝐴 ∈ 𝐵 ∧ 𝐴 ∈ dom 𝐹) → (𝐴 ∈ 𝐵 → 𝐴 ∈ dom 𝐹)) | 
| 26 | 1, 25 | sylbi 217 | . . . . . . . . 9
⊢ (𝐴 ∈ (𝐵 ∩ dom 𝐹) → (𝐴 ∈ 𝐵 → 𝐴 ∈ dom 𝐹)) | 
| 27 | 26, 3 | eleq2s 2858 | . . . . . . . 8
⊢ (𝐴 ∈ dom (𝐹 ↾ 𝐵) → (𝐴 ∈ 𝐵 → 𝐴 ∈ dom 𝐹)) | 
| 28 | 27 | com12 32 | . . . . . . 7
⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ dom (𝐹 ↾ 𝐵) → 𝐴 ∈ dom 𝐹)) | 
| 29 | 7 | funeqd 6587 | . . . . . . . 8
⊢ (𝐴 ∈ 𝐵 → (Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}) ↔ Fun (𝐹 ↾ {𝐴}))) | 
| 30 | 29 | biimpd 229 | . . . . . . 7
⊢ (𝐴 ∈ 𝐵 → (Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}) → Fun (𝐹 ↾ {𝐴}))) | 
| 31 | 28, 30 | anim12d 609 | . . . . . 6
⊢ (𝐴 ∈ 𝐵 → ((𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))) | 
| 32 | 31 | con3d 152 | . . . . 5
⊢ (𝐴 ∈ 𝐵 → (¬ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → ¬ (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})))) | 
| 33 | 32 | impcom 407 | . . . 4
⊢ ((¬
(𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → ¬ (𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴}))) | 
| 34 |  | afvnfundmuv 47156 | . . . . 5
⊢ (¬
(𝐹 ↾ 𝐵) defAt 𝐴 → ((𝐹 ↾ 𝐵)'''𝐴) = V) | 
| 35 | 13, 34 | sylnbir 331 | . . . 4
⊢ (¬
(𝐴 ∈ dom (𝐹 ↾ 𝐵) ∧ Fun ((𝐹 ↾ 𝐵) ↾ {𝐴})) → ((𝐹 ↾ 𝐵)'''𝐴) = V) | 
| 36 | 33, 35 | syl 17 | . . 3
⊢ ((¬
(𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)'''𝐴) = V) | 
| 37 |  | afvnfundmuv 47156 | . . . . . 6
⊢ (¬
𝐹 defAt 𝐴 → (𝐹'''𝐴) = V) | 
| 38 | 19, 37 | sylnbir 331 | . . . . 5
⊢ (¬
(𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹'''𝐴) = V) | 
| 39 | 38 | eqcomd 2742 | . . . 4
⊢ (¬
(𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → V = (𝐹'''𝐴)) | 
| 40 | 39 | adantr 480 | . . 3
⊢ ((¬
(𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → V = (𝐹'''𝐴)) | 
| 41 | 36, 40 | eqtrd 2776 | . 2
⊢ ((¬
(𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐴 ∈ 𝐵) → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) | 
| 42 | 24, 41 | pm2.61ian 811 | 1
⊢ (𝐴 ∈ 𝐵 → ((𝐹 ↾ 𝐵)'''𝐴) = (𝐹'''𝐴)) |