Step | Hyp | Ref
| Expression |
1 | | fnresdm 6000 |
. . . . . . . 8
⊢ (𝐹 Fn {𝐴} → (𝐹 ↾ {𝐴}) = 𝐹) |
2 | | fnfun 5988 |
. . . . . . . . 9
⊢ (𝐹 Fn {𝐴} → Fun 𝐹) |
3 | | funressn 6426 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝐹 ↾ {𝐴}) ⊆ {〈𝐴, (𝐹‘𝐴)〉}) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝐹 Fn {𝐴} → (𝐹 ↾ {𝐴}) ⊆ {〈𝐴, (𝐹‘𝐴)〉}) |
5 | 1, 4 | eqsstr3d 3640 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴} → 𝐹 ⊆ {〈𝐴, (𝐹‘𝐴)〉}) |
6 | 5 | sseld 3602 |
. . . . . 6
⊢ (𝐹 Fn {𝐴} → (𝑥 ∈ 𝐹 → 𝑥 ∈ {〈𝐴, (𝐹‘𝐴)〉})) |
7 | | elsni 4194 |
. . . . . 6
⊢ (𝑥 ∈ {〈𝐴, (𝐹‘𝐴)〉} → 𝑥 = 〈𝐴, (𝐹‘𝐴)〉) |
8 | 6, 7 | syl6 35 |
. . . . 5
⊢ (𝐹 Fn {𝐴} → (𝑥 ∈ 𝐹 → 𝑥 = 〈𝐴, (𝐹‘𝐴)〉)) |
9 | | df-fn 5891 |
. . . . . . . 8
⊢ (𝐹 Fn {𝐴} ↔ (Fun 𝐹 ∧ dom 𝐹 = {𝐴})) |
10 | | fnsnb.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
11 | 10 | snid 4208 |
. . . . . . . . . 10
⊢ 𝐴 ∈ {𝐴} |
12 | | eleq2 2690 |
. . . . . . . . . 10
⊢ (dom
𝐹 = {𝐴} → (𝐴 ∈ dom 𝐹 ↔ 𝐴 ∈ {𝐴})) |
13 | 11, 12 | mpbiri 248 |
. . . . . . . . 9
⊢ (dom
𝐹 = {𝐴} → 𝐴 ∈ dom 𝐹) |
14 | 13 | anim2i 593 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ dom 𝐹 = {𝐴}) → (Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹)) |
15 | 9, 14 | sylbi 207 |
. . . . . . 7
⊢ (𝐹 Fn {𝐴} → (Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹)) |
16 | | funfvop 6329 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝐴 ∈ dom 𝐹) → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) |
17 | 15, 16 | syl 17 |
. . . . . 6
⊢ (𝐹 Fn {𝐴} → 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹) |
18 | | eleq1 2689 |
. . . . . 6
⊢ (𝑥 = 〈𝐴, (𝐹‘𝐴)〉 → (𝑥 ∈ 𝐹 ↔ 〈𝐴, (𝐹‘𝐴)〉 ∈ 𝐹)) |
19 | 17, 18 | syl5ibrcom 237 |
. . . . 5
⊢ (𝐹 Fn {𝐴} → (𝑥 = 〈𝐴, (𝐹‘𝐴)〉 → 𝑥 ∈ 𝐹)) |
20 | 8, 19 | impbid 202 |
. . . 4
⊢ (𝐹 Fn {𝐴} → (𝑥 ∈ 𝐹 ↔ 𝑥 = 〈𝐴, (𝐹‘𝐴)〉)) |
21 | | velsn 4193 |
. . . 4
⊢ (𝑥 ∈ {〈𝐴, (𝐹‘𝐴)〉} ↔ 𝑥 = 〈𝐴, (𝐹‘𝐴)〉) |
22 | 20, 21 | syl6bbr 278 |
. . 3
⊢ (𝐹 Fn {𝐴} → (𝑥 ∈ 𝐹 ↔ 𝑥 ∈ {〈𝐴, (𝐹‘𝐴)〉})) |
23 | 22 | eqrdv 2620 |
. 2
⊢ (𝐹 Fn {𝐴} → 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) |
24 | | fvex 6201 |
. . . 4
⊢ (𝐹‘𝐴) ∈ V |
25 | 10, 24 | fnsn 5946 |
. . 3
⊢
{〈𝐴, (𝐹‘𝐴)〉} Fn {𝐴} |
26 | | fneq1 5979 |
. . 3
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} → (𝐹 Fn {𝐴} ↔ {〈𝐴, (𝐹‘𝐴)〉} Fn {𝐴})) |
27 | 25, 26 | mpbiri 248 |
. 2
⊢ (𝐹 = {〈𝐴, (𝐹‘𝐴)〉} → 𝐹 Fn {𝐴}) |
28 | 23, 27 | impbii 199 |
1
⊢ (𝐹 Fn {𝐴} ↔ 𝐹 = {〈𝐴, (𝐹‘𝐴)〉}) |