This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fullfunfv

Description: The function value of the full function of F agrees with F . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fullfunfv ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑥 = 𝐴 → ( FullFun 𝐹 ‘ 𝑥 ) = ( FullFun 𝐹 ‘ 𝐴 ) )
2 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( FullFun 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ) )
4 df-fullfun ⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )
5 4 fveq1i ⊢ ( FullFun 𝐹 ‘ 𝑥 ) = ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 )
6 disjdif ⊢ ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅
7 funpartfun ⊢ Fun Funpart 𝐹
8 funfn ⊢ ( Fun Funpart 𝐹 ↔ Funpart 𝐹 Fn dom Funpart 𝐹 )
9 7 8 mpbi ⊢ Funpart 𝐹 Fn dom Funpart 𝐹
10 0ex ⊢ ∅ ∈ V
11 10 fconst ⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ }
12 ffn ⊢ ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ } → ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) )
13 11 12 ax-mp ⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 )
14 fvun1 ⊢ ( ( 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 ⊢ ( ( ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ∧ 𝑥 ∈ dom Funpart 𝐹 ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
16 6 15 mpan ⊢ ( 𝑥 ∈ dom Funpart 𝐹 → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
17 vex ⊢ 𝑥 ∈ V
18 eldif ⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ↔ ( 𝑥 ∈ V ∧ ¬ 𝑥 ∈ dom Funpart 𝐹 ) )
19 17 18 mpbiran ⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ↔ ¬ 𝑥 ∈ dom Funpart 𝐹 )
20 fvun2 ⊢ ( ( 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 ⊢ ( ( ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ∧ 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) )
22 6 21 mpan ⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) )
23 10 fvconst2 ⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) → ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ‘ 𝑥 ) = ∅ )
24 22 23 eqtrd ⊢ ( 𝑥 ∈ ( V ∖ dom Funpart 𝐹 ) → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ∅ )
25 19 24 sylbir ⊢ ( ¬ 𝑥 ∈ dom Funpart 𝐹 → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ∅ )
26 ndmfv ⊢ ( ¬ 𝑥 ∈ dom Funpart 𝐹 → ( Funpart 𝐹 ‘ 𝑥 ) = ∅ )
27 25 26 eqtr4d ⊢ ( ¬ 𝑥 ∈ dom Funpart 𝐹 → ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 ) )
28 16 27 pm2.61i ⊢ ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) ‘ 𝑥 ) = ( Funpart 𝐹 ‘ 𝑥 )
29 funpartfv ⊢ ( Funpart 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
30 5 28 29 3eqtri ⊢ ( FullFun 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 )
31 3 30 vtoclg ⊢ ( 𝐴 ∈ V → ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
32 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( FullFun 𝐹 ‘ 𝐴 ) = ∅ )
33 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
34 32 33 eqtr4d ⊢ ( ¬ 𝐴 ∈ V → ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
35 31 34 pm2.61i ⊢ ( FullFun 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )