Step | Hyp | Ref
| Expression |
1 | | sneq 3378 |
. . . . . 6
⊢ (x = B →
{x} = {B}) |
2 | 1 | reseq2d 4555 |
. . . . 5
⊢ (x = B →
(𝐹 ↾ {x}) = (𝐹 ↾ {B})) |
3 | | fveq2 5121 |
. . . . . . 7
⊢ (x = B →
(𝐹‘x) = (𝐹‘B)) |
4 | | opeq12 3542 |
. . . . . . 7
⊢
((x = B ∧ (𝐹‘x) = (𝐹‘B)) → 〈x, (𝐹‘x)〉 = 〈B, (𝐹‘B)〉) |
5 | 3, 4 | mpdan 398 |
. . . . . 6
⊢ (x = B →
〈x, (𝐹‘x)〉 = 〈B, (𝐹‘B)〉) |
6 | 5 | sneqd 3380 |
. . . . 5
⊢ (x = B →
{〈x, (𝐹‘x)〉} = {〈B, (𝐹‘B)〉}) |
7 | 2, 6 | eqeq12d 2051 |
. . . 4
⊢ (x = B →
((𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉} ↔ (𝐹 ↾ {B}) = {〈B,
(𝐹‘B)〉})) |
8 | 7 | imbi2d 219 |
. . 3
⊢ (x = B →
((𝐹 Fn A → (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉}) ↔ (𝐹 Fn A
→ (𝐹 ↾ {B}) = {〈B,
(𝐹‘B)〉}))) |
9 | | vex 2554 |
. . . . . . 7
⊢ x ∈
V |
10 | 9 | snss 3485 |
. . . . . 6
⊢ (x ∈ A ↔ {x}
⊆ A) |
11 | | fnssres 4955 |
. . . . . 6
⊢ ((𝐹 Fn A ∧ {x} ⊆ A)
→ (𝐹 ↾ {x}) Fn {x}) |
12 | 10, 11 | sylan2b 271 |
. . . . 5
⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) Fn {x}) |
13 | | dffn2 4990 |
. . . . . . 7
⊢ ((𝐹 ↾ {x}) Fn {x}
↔ (𝐹 ↾ {x}):{x}⟶V) |
14 | 9 | fsn2 5280 |
. . . . . . 7
⊢ ((𝐹 ↾ {x}):{x}⟶V
↔ (((𝐹 ↾
{x})‘x) ∈ V ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉})) |
15 | 13, 14 | bitri 173 |
. . . . . 6
⊢ ((𝐹 ↾ {x}) Fn {x}
↔ (((𝐹 ↾
{x})‘x) ∈ V ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉})) |
16 | | ssnid 3395 |
. . . . . . . . . . 11
⊢ x ∈ {x} |
17 | | fvres 5141 |
. . . . . . . . . . 11
⊢ (x ∈ {x} → ((𝐹 ↾ {x})‘x) =
(𝐹‘x)) |
18 | 16, 17 | ax-mp 7 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ {x})‘x) =
(𝐹‘x) |
19 | 18 | opeq2i 3544 |
. . . . . . . . 9
⊢
〈x, ((𝐹 ↾ {x})‘x)〉 = 〈x, (𝐹‘x)〉 |
20 | 19 | sneqi 3379 |
. . . . . . . 8
⊢
{〈x, ((𝐹 ↾ {x})‘x)〉} = {〈x, (𝐹‘x)〉} |
21 | 20 | eqeq2i 2047 |
. . . . . . 7
⊢ ((𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉} ↔ (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉}) |
22 | | snssi 3499 |
. . . . . . . . . 10
⊢ (x ∈ A → {x}
⊆ A) |
23 | 22, 11 | sylan2 270 |
. . . . . . . . 9
⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) Fn {x}) |
24 | | funfvex 5135 |
. . . . . . . . . 10
⊢ ((Fun
(𝐹 ↾ {x}) ∧ x ∈ dom (𝐹 ↾ {x})) → ((𝐹 ↾ {x})‘x)
∈ V) |
25 | 24 | funfni 4942 |
. . . . . . . . 9
⊢ (((𝐹 ↾ {x}) Fn {x} ∧ x ∈ {x}) →
((𝐹 ↾ {x})‘x)
∈ V) |
26 | 23, 16, 25 | sylancl 392 |
. . . . . . . 8
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x})‘x)
∈ V) |
27 | 26 | biantrurd 289 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉} ↔ (((𝐹 ↾ {x})‘x)
∈ V ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉}))) |
28 | 21, 27 | syl5rbbr 184 |
. . . . . 6
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((((𝐹 ↾ {x})‘x)
∈ V ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉}) ↔ (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉})) |
29 | 15, 28 | syl5bb 181 |
. . . . 5
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x}) Fn {x}
↔ (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉})) |
30 | 12, 29 | mpbid 135 |
. . . 4
⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉}) |
31 | 30 | expcom 109 |
. . 3
⊢ (x ∈ A → (𝐹 Fn A
→ (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉})) |
32 | 8, 31 | vtoclga 2613 |
. 2
⊢ (B ∈ A → (𝐹 Fn A
→ (𝐹 ↾ {B}) = {〈B,
(𝐹‘B)〉})) |
33 | 32 | impcom 116 |
1
⊢ ((𝐹 Fn A ∧ B ∈ A) → (𝐹 ↾ {B}) = {〈B,
(𝐹‘B)〉}) |