Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . 4
⊢ (𝑥 = 𝐴 → (FullFun𝐹‘𝑥) = (FullFun𝐹‘𝐴)) |
2 | | fveq2 6191 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝐹‘𝑥) = (𝐹‘𝐴)) |
3 | 1, 2 | eqeq12d 2637 |
. . 3
⊢ (𝑥 = 𝐴 → ((FullFun𝐹‘𝑥) = (𝐹‘𝑥) ↔ (FullFun𝐹‘𝐴) = (𝐹‘𝐴))) |
4 | | df-fullfun 31982 |
. . . . 5
⊢
FullFun𝐹 =
(Funpart𝐹 ∪ ((V ∖
dom Funpart𝐹) ×
{∅})) |
5 | 4 | fveq1i 6192 |
. . . 4
⊢
(FullFun𝐹‘𝑥) = ((Funpart𝐹 ∪ ((V ∖ dom Funpart𝐹) ×
{∅}))‘𝑥) |
6 | | disjdif 4040 |
. . . . . 6
⊢ (dom
Funpart𝐹 ∩ (V ∖
dom Funpart𝐹)) =
∅ |
7 | | funpartfun 32050 |
. . . . . . . 8
⊢ Fun
Funpart𝐹 |
8 | | funfn 5918 |
. . . . . . . 8
⊢ (Fun
Funpart𝐹 ↔
Funpart𝐹 Fn dom
Funpart𝐹) |
9 | 7, 8 | mpbi 220 |
. . . . . . 7
⊢
Funpart𝐹 Fn dom
Funpart𝐹 |
10 | | 0ex 4790 |
. . . . . . . . 9
⊢ ∅
∈ V |
11 | 10 | fconst 6091 |
. . . . . . . 8
⊢ ((V
∖ dom Funpart𝐹)
× {∅}):(V ∖ dom Funpart𝐹)⟶{∅} |
12 | | ffn 6045 |
. . . . . . . 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 6269 |
. . . . . . 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 1414 |
. . . . . 6
⊢ (((dom
Funpart𝐹 ∩ (V ∖
dom Funpart𝐹)) = ∅
∧ 𝑥 ∈ dom
Funpart𝐹) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (Funpart𝐹‘𝑥)) |
16 | 6, 15 | mpan 706 |
. . . . 5
⊢ (𝑥 ∈ dom Funpart𝐹 → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
(Funpart𝐹‘𝑥)) |
17 | | vex 3203 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
18 | | eldif 3584 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) ↔ (𝑥 ∈ V ∧ ¬ 𝑥 ∈ dom Funpart𝐹)) |
19 | 17, 18 | mpbiran 953 |
. . . . . . 7
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) ↔ ¬
𝑥 ∈ dom Funpart𝐹) |
20 | | fvun2 6270 |
. . . . . . . . . 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 1414 |
. . . . . . . . 9
⊢ (((dom
Funpart𝐹 ∩ (V ∖
dom Funpart𝐹)) = ∅
∧ 𝑥 ∈ (V ∖
dom Funpart𝐹)) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (((V ∖ dom Funpart𝐹) × {∅})‘𝑥)) |
22 | 6, 21 | mpan 706 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (((V ∖ dom Funpart𝐹) × {∅})‘𝑥)) |
23 | 10 | fvconst2 6469 |
. . . . . . . 8
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) → (((V
∖ dom Funpart𝐹)
× {∅})‘𝑥)
= ∅) |
24 | 22, 23 | eqtrd 2656 |
. . . . . . 7
⊢ (𝑥 ∈ (V ∖ dom
Funpart𝐹) →
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = ∅) |
25 | 19, 24 | sylbir 225 |
. . . . . 6
⊢ (¬
𝑥 ∈ dom Funpart𝐹 → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
∅) |
26 | | ndmfv 6218 |
. . . . . 6
⊢ (¬
𝑥 ∈ dom Funpart𝐹 → (Funpart𝐹‘𝑥) = ∅) |
27 | 25, 26 | eqtr4d 2659 |
. . . . 5
⊢ (¬
𝑥 ∈ dom Funpart𝐹 → ((Funpart𝐹 ∪ ((V ∖ dom
Funpart𝐹) ×
{∅}))‘𝑥) =
(Funpart𝐹‘𝑥)) |
28 | 16, 27 | pm2.61i 176 |
. . . 4
⊢
((Funpart𝐹 ∪ ((V
∖ dom Funpart𝐹)
× {∅}))‘𝑥) = (Funpart𝐹‘𝑥) |
29 | | funpartfv 32052 |
. . . 4
⊢
(Funpart𝐹‘𝑥) = (𝐹‘𝑥) |
30 | 5, 28, 29 | 3eqtri 2648 |
. . 3
⊢
(FullFun𝐹‘𝑥) = (𝐹‘𝑥) |
31 | 3, 30 | vtoclg 3266 |
. 2
⊢ (𝐴 ∈ V → (FullFun𝐹‘𝐴) = (𝐹‘𝐴)) |
32 | | fvprc 6185 |
. . 3
⊢ (¬
𝐴 ∈ V →
(FullFun𝐹‘𝐴) = ∅) |
33 | | fvprc 6185 |
. . 3
⊢ (¬
𝐴 ∈ V → (𝐹‘𝐴) = ∅) |
34 | 32, 33 | eqtr4d 2659 |
. 2
⊢ (¬
𝐴 ∈ V →
(FullFun𝐹‘𝐴) = (𝐹‘𝐴)) |
35 | 31, 34 | pm2.61i 176 |
1
⊢
(FullFun𝐹‘𝐴) = (𝐹‘𝐴) |