Step | Hyp | Ref
| Expression |
1 | | sneq 3538 |
. . . . . 6
⊢ (𝑥 = 𝐵 → {𝑥} = {𝐵}) |
2 | 1 | reseq2d 4819 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐹 ↾ {𝑥}) = (𝐹 ↾ {𝐵})) |
3 | | fveq2 5421 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
4 | | opeq12 3707 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ (𝐹‘𝑥) = (𝐹‘𝐵)) → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
5 | 3, 4 | mpdan 417 |
. . . . . 6
⊢ (𝑥 = 𝐵 → 〈𝑥, (𝐹‘𝑥)〉 = 〈𝐵, (𝐹‘𝐵)〉) |
6 | 5 | sneqd 3540 |
. . . . 5
⊢ (𝑥 = 𝐵 → {〈𝑥, (𝐹‘𝑥)〉} = {〈𝐵, (𝐹‘𝐵)〉}) |
7 | 2, 6 | eqeq12d 2154 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉} ↔ (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) |
8 | 7 | imbi2d 229 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) ↔ (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}))) |
9 | | vex 2689 |
. . . . . . 7
⊢ 𝑥 ∈ V |
10 | 9 | snss 3649 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | | fnssres 5236 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ {𝑥} ⊆ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
12 | 10, 11 | sylan2b 285 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
13 | | dffn2 5274 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}):{𝑥}⟶V) |
14 | 9 | fsn2 5594 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}):{𝑥}⟶V ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) |
15 | 13, 14 | bitri 183 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉})) |
16 | | vsnid 3557 |
. . . . . . . . . . 11
⊢ 𝑥 ∈ {𝑥} |
17 | | fvres 5445 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥)) |
18 | 16, 17 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥) |
19 | 18 | opeq2i 3709 |
. . . . . . . . 9
⊢
〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉 = 〈𝑥, (𝐹‘𝑥)〉 |
20 | 19 | sneqi 3539 |
. . . . . . . 8
⊢
{〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} = {〈𝑥, (𝐹‘𝑥)〉} |
21 | 20 | eqeq2i 2150 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
22 | | snssi 3664 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) |
23 | 22, 11 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
24 | | funfvex 5438 |
. . . . . . . . . 10
⊢ ((Fun
(𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom (𝐹 ↾ {𝑥})) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) |
25 | 24 | funfni 5223 |
. . . . . . . . 9
⊢ (((𝐹 ↾ {𝑥}) Fn {𝑥} ∧ 𝑥 ∈ {𝑥}) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) |
26 | 23, 16, 25 | sylancl 409 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) |
27 | 26 | biantrurd 303 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉}))) |
28 | 21, 27 | syl5rbbr 194 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {〈𝑥, ((𝐹 ↾ {𝑥})‘𝑥)〉}) ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) |
29 | 15, 28 | syl5bb 191 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) |
30 | 12, 29 | mpbid 146 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉}) |
31 | 30 | expcom 115 |
. . 3
⊢ (𝑥 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {〈𝑥, (𝐹‘𝑥)〉})) |
32 | 8, 31 | vtoclga 2752 |
. 2
⊢ (𝐵 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉})) |
33 | 32 | impcom 124 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {〈𝐵, (𝐹‘𝐵)〉}) |