Step | Hyp | Ref
| Expression |
1 | | sneq 3378 |
. . . . . 6
⊢ (x = B →
{x} = {B}) |
2 | | reseq2 4550 |
. . . . . . . 8
⊢
({x} = {B} → (𝐹 ↾ {x}) = (𝐹 ↾ {B})) |
3 | 2 | feq1d 4977 |
. . . . . . 7
⊢
({x} = {B} → ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹 ↾ {B}):{x}⟶𝐶)) |
4 | | feq2 4974 |
. . . . . . 7
⊢
({x} = {B} → ((𝐹 ↾ {B}):{x}⟶𝐶 ↔ (𝐹 ↾ {B}):{B}⟶𝐶)) |
5 | 3, 4 | bitrd 177 |
. . . . . 6
⊢
({x} = {B} → ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹 ↾ {B}):{B}⟶𝐶)) |
6 | 1, 5 | syl 14 |
. . . . 5
⊢ (x = B →
((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹 ↾ {B}):{B}⟶𝐶)) |
7 | | fveq2 5121 |
. . . . . 6
⊢ (x = B →
(𝐹‘x) = (𝐹‘B)) |
8 | 7 | eleq1d 2103 |
. . . . 5
⊢ (x = B →
((𝐹‘x) ∈ 𝐶 ↔ (𝐹‘B) ∈ 𝐶)) |
9 | 6, 8 | bibi12d 224 |
. . . 4
⊢ (x = B →
(((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹‘x) ∈ 𝐶) ↔ ((𝐹 ↾ {B}):{B}⟶𝐶 ↔ (𝐹‘B) ∈ 𝐶))) |
10 | 9 | imbi2d 219 |
. . 3
⊢ (x = B →
((𝐹 Fn A → ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹‘x) ∈ 𝐶)) ↔ (𝐹 Fn A
→ ((𝐹 ↾
{B}):{B}⟶𝐶 ↔ (𝐹‘B) ∈ 𝐶)))) |
11 | | fnressn 5292 |
. . . . 5
⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉}) |
12 | | ssnid 3395 |
. . . . . . . . . 10
⊢ x ∈ {x} |
13 | | fvres 5141 |
. . . . . . . . . 10
⊢ (x ∈ {x} → ((𝐹 ↾ {x})‘x) =
(𝐹‘x)) |
14 | 12, 13 | ax-mp 7 |
. . . . . . . . 9
⊢ ((𝐹 ↾ {x})‘x) =
(𝐹‘x) |
15 | 14 | opeq2i 3544 |
. . . . . . . 8
⊢
〈x, ((𝐹 ↾ {x})‘x)〉 = 〈x, (𝐹‘x)〉 |
16 | 15 | sneqi 3379 |
. . . . . . 7
⊢
{〈x, ((𝐹 ↾ {x})‘x)〉} = {〈x, (𝐹‘x)〉} |
17 | 16 | eqeq2i 2047 |
. . . . . 6
⊢ ((𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉} ↔ (𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉}) |
18 | | vex 2554 |
. . . . . . . 8
⊢ x ∈
V |
19 | 18 | fsn2 5280 |
. . . . . . 7
⊢ ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (((𝐹 ↾ {x})‘x)
∈ 𝐶 ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉})) |
20 | 14 | eleq1i 2100 |
. . . . . . . 8
⊢ (((𝐹 ↾ {x})‘x)
∈ 𝐶 ↔ (𝐹‘x) ∈ 𝐶) |
21 | | iba 284 |
. . . . . . . 8
⊢ ((𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉} → (((𝐹 ↾ {x})‘x)
∈ 𝐶 ↔ (((𝐹 ↾ {x})‘x)
∈ 𝐶 ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉}))) |
22 | 20, 21 | syl5rbbr 184 |
. . . . . . 7
⊢ ((𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉} → ((((𝐹 ↾ {x})‘x)
∈ 𝐶 ∧ (𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉}) ↔ (𝐹‘x) ∈ 𝐶)) |
23 | 19, 22 | syl5bb 181 |
. . . . . 6
⊢ ((𝐹 ↾ {x}) = {〈x,
((𝐹 ↾ {x})‘x)〉} → ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹‘x) ∈ 𝐶)) |
24 | 17, 23 | sylbir 125 |
. . . . 5
⊢ ((𝐹 ↾ {x}) = {〈x,
(𝐹‘x)〉} → ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹‘x) ∈ 𝐶)) |
25 | 11, 24 | syl 14 |
. . . 4
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹 ↾ {x}):{x}⟶𝐶 ↔ (𝐹‘x) ∈ 𝐶)) |
26 | 25 | expcom 109 |
. . 3
⊢ (x ∈ A → (𝐹 Fn A
→ ((𝐹 ↾
{x}):{x}⟶𝐶 ↔ (𝐹‘x) ∈ 𝐶))) |
27 | 10, 26 | vtoclga 2613 |
. 2
⊢ (B ∈ A → (𝐹 Fn A
→ ((𝐹 ↾
{B}):{B}⟶𝐶 ↔ (𝐹‘B) ∈ 𝐶))) |
28 | 27 | impcom 116 |
1
⊢ ((𝐹 Fn A ∧ B ∈ A) → ((𝐹 ↾ {B}):{B}⟶𝐶 ↔ (𝐹‘B) ∈ 𝐶)) |