Step | Hyp | Ref
| Expression |
1 | | sneq 3605 |
. . . . . 6
⊢ (𝑥 = 𝐵 → {𝑥} = {𝐵}) |
2 | 1 | reseq2d 4909 |
. . . . 5
⊢ (𝑥 = 𝐵 → (𝐹 ↾ {𝑥}) = (𝐹 ↾ {𝐵})) |
3 | | fveq2 5517 |
. . . . . . 7
⊢ (𝑥 = 𝐵 → (𝐹‘𝑥) = (𝐹‘𝐵)) |
4 | | opeq12 3782 |
. . . . . . 7
⊢ ((𝑥 = 𝐵 ∧ (𝐹‘𝑥) = (𝐹‘𝐵)) → ⟨𝑥, (𝐹‘𝑥)⟩ = ⟨𝐵, (𝐹‘𝐵)⟩) |
5 | 3, 4 | mpdan 421 |
. . . . . 6
⊢ (𝑥 = 𝐵 → ⟨𝑥, (𝐹‘𝑥)⟩ = ⟨𝐵, (𝐹‘𝐵)⟩) |
6 | 5 | sneqd 3607 |
. . . . 5
⊢ (𝑥 = 𝐵 → {⟨𝑥, (𝐹‘𝑥)⟩} = {⟨𝐵, (𝐹‘𝐵)⟩}) |
7 | 2, 6 | eqeq12d 2192 |
. . . 4
⊢ (𝑥 = 𝐵 → ((𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩} ↔ (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩})) |
8 | 7 | imbi2d 230 |
. . 3
⊢ (𝑥 = 𝐵 → ((𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩}) ↔ (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩}))) |
9 | | vex 2742 |
. . . . . . 7
⊢ 𝑥 ∈ V |
10 | 9 | snss 3729 |
. . . . . 6
⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴) |
11 | | fnssres 5331 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ {𝑥} ⊆ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
12 | 10, 11 | sylan2b 287 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
13 | | dffn2 5369 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}):{𝑥}⟶V) |
14 | 9 | fsn2 5692 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}):{𝑥}⟶V ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩})) |
15 | 13, 14 | bitri 184 |
. . . . . 6
⊢ ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩})) |
16 | | snssi 3738 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴) |
17 | 16, 11 | sylan2 286 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) Fn {𝑥}) |
18 | | vsnid 3626 |
. . . . . . . . 9
⊢ 𝑥 ∈ {𝑥} |
19 | | funfvex 5534 |
. . . . . . . . . 10
⊢ ((Fun
(𝐹 ↾ {𝑥}) ∧ 𝑥 ∈ dom (𝐹 ↾ {𝑥})) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) |
20 | 19 | funfni 5318 |
. . . . . . . . 9
⊢ (((𝐹 ↾ {𝑥}) Fn {𝑥} ∧ 𝑥 ∈ {𝑥}) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) |
21 | 17, 18, 20 | sylancl 413 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥})‘𝑥) ∈ V) |
22 | 21 | biantrurd 305 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥}) = {⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩} ↔ (((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩}))) |
23 | | fvres 5541 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑥} → ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥)) |
24 | 18, 23 | ax-mp 5 |
. . . . . . . . . 10
⊢ ((𝐹 ↾ {𝑥})‘𝑥) = (𝐹‘𝑥) |
25 | 24 | opeq2i 3784 |
. . . . . . . . 9
⊢
⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩ = ⟨𝑥, (𝐹‘𝑥)⟩ |
26 | 25 | sneqi 3606 |
. . . . . . . 8
⊢
{⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩} = {⟨𝑥, (𝐹‘𝑥)⟩} |
27 | 26 | eqeq2i 2188 |
. . . . . . 7
⊢ ((𝐹 ↾ {𝑥}) = {⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩} ↔ (𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩}) |
28 | 22, 27 | bitr3di 195 |
. . . . . 6
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((((𝐹 ↾ {𝑥})‘𝑥) ∈ V ∧ (𝐹 ↾ {𝑥}) = {⟨𝑥, ((𝐹 ↾ {𝑥})‘𝑥)⟩}) ↔ (𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩})) |
29 | 15, 28 | bitrid 192 |
. . . . 5
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹 ↾ {𝑥}) Fn {𝑥} ↔ (𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩})) |
30 | 12, 29 | mpbid 147 |
. . . 4
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩}) |
31 | 30 | expcom 116 |
. . 3
⊢ (𝑥 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝑥}) = {⟨𝑥, (𝐹‘𝑥)⟩})) |
32 | 8, 31 | vtoclga 2805 |
. 2
⊢ (𝐵 ∈ 𝐴 → (𝐹 Fn 𝐴 → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩})) |
33 | 32 | impcom 125 |
1
⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐹 ↾ {𝐵}) = {⟨𝐵, (𝐹‘𝐵)⟩}) |