Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . . 4
⊢ (𝐹''''𝐴) = (𝐹''''𝐴) |
2 | | dfatafv2ex 44285 |
. . . . . 6
⊢ (𝐹 defAt 𝐴 → (𝐹''''𝐴) ∈ V) |
3 | 2 | adantr 484 |
. . . . 5
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → (𝐹''''𝐴) ∈ V) |
4 | | eqeq2 2751 |
. . . . . . 7
⊢ (𝑥 = (𝐹''''𝐴) → ((𝐹''''𝐴) = 𝑥 ↔ (𝐹''''𝐴) = (𝐹''''𝐴))) |
5 | | breq2 5044 |
. . . . . . 7
⊢ (𝑥 = (𝐹''''𝐴) → (𝐴𝐹𝑥 ↔ 𝐴𝐹(𝐹''''𝐴))) |
6 | 4, 5 | bibi12d 349 |
. . . . . 6
⊢ (𝑥 = (𝐹''''𝐴) → (((𝐹''''𝐴) = 𝑥 ↔ 𝐴𝐹𝑥) ↔ ((𝐹''''𝐴) = (𝐹''''𝐴) ↔ 𝐴𝐹(𝐹''''𝐴)))) |
7 | 6 | adantl 485 |
. . . . 5
⊢ (((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) ∧ 𝑥 = (𝐹''''𝐴)) → (((𝐹''''𝐴) = 𝑥 ↔ 𝐴𝐹𝑥) ↔ ((𝐹''''𝐴) = (𝐹''''𝐴) ↔ 𝐴𝐹(𝐹''''𝐴)))) |
8 | | dfdfat2 44200 |
. . . . . . 7
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ ∃!𝑥 𝐴𝐹𝑥)) |
9 | | tz6.12c-afv2 44314 |
. . . . . . 7
⊢
(∃!𝑥 𝐴𝐹𝑥 → ((𝐹''''𝐴) = 𝑥 ↔ 𝐴𝐹𝑥)) |
10 | 8, 9 | simplbiim 508 |
. . . . . 6
⊢ (𝐹 defAt 𝐴 → ((𝐹''''𝐴) = 𝑥 ↔ 𝐴𝐹𝑥)) |
11 | 10 | adantr 484 |
. . . . 5
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝐹''''𝐴) = 𝑥 ↔ 𝐴𝐹𝑥)) |
12 | 3, 7, 11 | vtocld 3462 |
. . . 4
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝐹''''𝐴) = (𝐹''''𝐴) ↔ 𝐴𝐹(𝐹''''𝐴))) |
13 | 1, 12 | mpbii 236 |
. . 3
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → 𝐴𝐹(𝐹''''𝐴)) |
14 | | breq2 5044 |
. . 3
⊢ ((𝐹''''𝐴) = 𝐵 → (𝐴𝐹(𝐹''''𝐴) ↔ 𝐴𝐹𝐵)) |
15 | 13, 14 | syl5ibcom 248 |
. 2
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝐹''''𝐴) = 𝐵 → 𝐴𝐹𝐵)) |
16 | | df-dfat 44191 |
. . . 4
⊢ (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))) |
17 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐵 ∈ 𝑊) → 𝐴 ∈ dom 𝐹) |
18 | | simpr 488 |
. . . . 5
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐵 ∈ 𝑊) → 𝐵 ∈ 𝑊) |
19 | | simpr 488 |
. . . . . 6
⊢ ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → Fun (𝐹 ↾ {𝐴})) |
20 | 19 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐵 ∈ 𝑊) → Fun (𝐹 ↾ {𝐴})) |
21 | 17, 18, 20 | jca31 518 |
. . . 4
⊢ (((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}))) |
22 | 16, 21 | sylanb 584 |
. . 3
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴}))) |
23 | | funressnbrafv2 44316 |
. . 3
⊢ (((𝐴 ∈ dom 𝐹 ∧ 𝐵 ∈ 𝑊) ∧ Fun (𝐹 ↾ {𝐴})) → (𝐴𝐹𝐵 → (𝐹''''𝐴) = 𝐵)) |
24 | 22, 23 | syl 17 |
. 2
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → (𝐴𝐹𝐵 → (𝐹''''𝐴) = 𝐵)) |
25 | 15, 24 | impbid 215 |
1
⊢ ((𝐹 defAt 𝐴 ∧ 𝐵 ∈ 𝑊) → ((𝐹''''𝐴) = 𝐵 ↔ 𝐴𝐹𝐵)) |