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 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V

Proof

Step Hyp Ref Expression
1 funpartfun Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
2 funfn Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
3 1 2 mpbi 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
4 0ex V
5 4 fconst V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × : V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
6 ffn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × : V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
7 5 6 ax-mp V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
8 3 7 pm3.2i 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
9 disjdif dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F =
10 fnun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
11 8 9 10 mp2an 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
12 df-fullfun 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ×
13 12 fneq1i 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V
14 unvdif dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = V
15 14 eqcomi V = dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
16 15 fneq2i 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
17 13 16 bitri 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
18 11 17 mpbir 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F Fn V