Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . 4
⊢ (𝑥 = 𝐴 → (FullFun𝐹‘𝑥) = (FullFun𝐹‘𝐴)) |
2 | | fveq2 6717 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
3 | 1, 2 | eqeq12d 2753 |
. . 3
⊢ (𝑥 = 𝐴 → ((FullFun𝐹‘𝑥) = (𝐹‘𝑥) ↔ (FullFun𝐹‘𝐴) = (𝐹‘𝐴))) |
4 | | df-fullfun 33914 |
. . . . 5
⊢
FullFun𝐹 =
(Funpart𝐹 ∪ ((V ∖
dom Funpart𝐹) ×
{∅})) |
5 | 4 | fveq1i 6718 |
. . . 4
⊢
(FullFun𝐹‘𝑥) = ((Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) ×
{∅}))‘𝑥) |
6 | | disjdif 4386 |
. . . . . 6
⊢ (dom
Funpart𝐹 ∩ (V ∖
dom Funpart𝐹)) =
∅ |
7 | | funpartfun 33982 |
. . . . . . . 8
⊢ Fun
Funpart𝐹 |
8 | | funfn 6410 |
. . . . . . . 8
⊢ (Fun
Funpart𝐹 ↔
Funpart𝐹 Fn dom
Funpart𝐹) |
9 | 7, 8 | mpbi 233 |
. . . . . . 7
⊢
Funpart𝐹 Fn dom
Funpart𝐹 |
10 | | 0ex 5200 |
. . . . . . . . 9
⊢ ∅
∈ V |
11 | 10 | fconst 6605 |
. . . . . . . 8
⊢ ((V
∖ dom Funpart𝐹)
× {∅}):(V ∖ dom Funpart𝐹)⟶{∅} |
12 | | ffn 6545 |
. . . . . . . 8
⊢ (((V
∖ dom Funpart𝐹)
× {∅}):(V ∖ dom Funpart𝐹)⟶{∅} → ((V ∖ dom
Funpart𝐹) ×
{∅}) Fn (V ∖ dom Funpart𝐹)) |
13 | 11, 12 | ax-mp 5 |
. . . . . . 7
⊢ ((V
∖ dom Funpart𝐹)
× {∅}) Fn (V ∖ dom Funpart𝐹) |
14 | | fvun1 6802 |
. . . . . . 7
⊢
((Funpart𝐹 Fn dom
Funpart𝐹 ∧ ((V ∖
dom Funpart𝐹) ×
{∅}) Fn (V ∖ dom Funpart𝐹) ∧ ((dom Funpart𝐹 ∩ (V ∖ dom Funpart𝐹)) = ∅ ∧ 𝑥 ∈ dom Funpart𝐹)) → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
(Funpart𝐹‘𝑥)) |
15 | 9, 13, 14 | mp3an12 1453 |
. . . . . 6
⊢ (((dom
Funpart𝐹 ∩ (V ∖
dom Funpart𝐹)) = ∅
∧ 𝑥 ∈ dom
Funpart𝐹) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (Funpart𝐹‘𝑥)) |
16 | 6, 15 | mpan 690 |
. . . . 5
⊢ (𝑥 ∈ dom Funpart𝐹 → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
(Funpart𝐹‘𝑥)) |
17 | | vex 3412 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
18 | | eldif 3876 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ dom Funpart𝐹)) |
19 | 17, 18 | mpbiran 709 |
. . . . . . 7
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) ↔ ¬
𝑥 ∈ dom Funpart𝐹) |
20 | | fvun2 6803 |
. . . . . . . . . 10
⊢
((Funpart𝐹 Fn dom
Funpart𝐹 ∧ ((V ∖
dom Funpart𝐹) ×
{∅}) Fn (V ∖ dom Funpart𝐹) ∧ ((dom Funpart𝐹 ∩ (V ∖ dom Funpart𝐹)) = ∅ ∧ 𝑥 ∈ (V ∖ dom
Funpart𝐹))) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (((V ∖ dom Funpart𝐹) × {∅})‘𝑥)) |
21 | 9, 13, 20 | mp3an12 1453 |
. . . . . . . . 9
⊢ (((dom
Funpart𝐹 ∩ (V ∖
dom Funpart𝐹)) = ∅
∧ 𝑥 ∈ (V ∖
dom Funpart𝐹)) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (((V ∖ dom Funpart𝐹) × {∅})‘𝑥)) |
22 | 6, 21 | mpan 690 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (((V ∖ dom Funpart𝐹) × {∅})‘𝑥)) |
23 | 10 | fvconst2 7019 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) → (((V
∖ dom Funpart𝐹)
× {∅})‘𝑥)
= ∅) |
24 | 22, 23 | eqtrd 2777 |
. . . . . . 7
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = ∅) |
25 | 19, 24 | sylbir 238 |
. . . . . 6
⊢ (¬
𝑥 ∈ dom Funpart𝐹 → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
∅) |
26 | | ndmfv 6747 |
. . . . . 6
⊢ (¬
𝑥 ∈ dom Funpart𝐹 → (Funpart𝐹‘𝑥) = ∅) |
27 | 25, 26 | eqtr4d 2780 |
. . . . 5
⊢ (¬
𝑥 ∈ dom Funpart𝐹 → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
(Funpart𝐹‘𝑥)) |
28 | 16, 27 | pm2.61i 185 |
. . . 4
⊢
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (Funpart𝐹‘𝑥) |
29 | | funpartfv 33984 |
. . . 4
⊢
(Funpart𝐹‘𝑥) = (𝐹‘𝑥) |
30 | 5, 28, 29 | 3eqtri 2769 |
. . 3
⊢
(FullFun𝐹‘𝑥) = (𝐹‘𝑥) |
31 | 3, 30 | vtoclg 3481 |
. 2
⊢ (𝐴 ∈ V → (FullFun𝐹‘𝐴) = (𝐹‘𝐴)) |
32 | | fvprc 6709 |
. . 3
⊢ (¬
𝐴 ∈ V →
(FullFun𝐹‘𝐴) = ∅) |
33 | | fvprc 6709 |
. . 3
⊢ (¬
𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
34 | 32, 33 | eqtr4d 2780 |
. 2
⊢ (¬
𝐴 ∈ V →
(FullFun𝐹‘𝐴) = (𝐹‘𝐴)) |
35 | 31, 34 | pm2.61i 185 |
1
⊢
(FullFun𝐹‘𝐴) = (𝐹‘𝐴) |