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

Metamath Proof Explorer

Theorem fullfunfnv

Description: The full functional part of F is a function over _V . (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fullfunfnv FullFun 𝐹 Fn V

Proof

Step Hyp Ref Expression
1 funpartfun ⊢ Fun Funpart 𝐹
2 funfn ⊢ ( Fun Funpart 𝐹 ↔ Funpart 𝐹 Fn dom Funpart 𝐹 )
3 1 2 mpbi ⊢ Funpart 𝐹 Fn dom Funpart 𝐹
4 0ex ⊢ ∅ ∈ V
5 4 fconst ⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ }
6 ffn ⊢ ( ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) : ( V ∖ dom Funpart 𝐹 ) ⟶ { ∅ } → ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) )
7 5 6 ax-mp ⊢ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 )
8 3 7 pm3.2i ⊢ ( Funpart 𝐹 Fn dom Funpart 𝐹 ∧ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) )
9 disjdif ⊢ ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅
10 fnun ⊢ ( ( ( Funpart 𝐹 Fn dom Funpart 𝐹 ∧ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) Fn ( V ∖ dom Funpart 𝐹 ) ) ∧ ( dom Funpart 𝐹 ∩ ( V ∖ dom Funpart 𝐹 ) ) = ∅ ) → ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) )
11 8 9 10 mp2an ⊢ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) )
12 df-fullfun ⊢ FullFun 𝐹 = ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) )
13 12 fneq1i ⊢ ( FullFun 𝐹 Fn V ↔ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn V )
14 unvdif ⊢ ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) = V
15 14 eqcomi ⊢ V = ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) )
16 15 fneq2i ⊢ ( ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn V ↔ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) )
17 13 16 bitri ⊢ ( FullFun 𝐹 Fn V ↔ ( Funpart 𝐹 ∪ ( ( V ∖ dom Funpart 𝐹 ) × { ∅ } ) ) Fn ( dom Funpart 𝐹 ∪ ( V ∖ dom Funpart 𝐹 ) ) )
18 11 17 mpbir ⊢ FullFun 𝐹 Fn V