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 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A = F A

Proof

Step Hyp Ref Expression
1 fveq2 x = A 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x = 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A
2 fveq2 x = A F x = F A
3 1 2 eqeq12d x = A 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x = F x 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A = F A
4 df-fullfun 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ×
5 4 fveq1i 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x
6 disjdif dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F =
7 funpartfun Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
8 funfn Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
9 7 8 mpbi 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
10 0ex V
11 10 fconst V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × : V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
12 ffn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × : V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
13 11 12 ax-mp V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
14 fvun1 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x
15 9 13 14 mp3an12 dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x
16 6 15 mpan x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x
17 vex x V
18 eldif x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x V ¬ x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
19 17 18 mpbiran x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F ¬ x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F
20 fvun2 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fn dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × Fn V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x
21 9 13 20 mp3an12 dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x
22 6 21 mpan x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x
23 10 fvconst2 x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x =
24 22 23 eqtrd x V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x =
25 19 24 sylbir ¬ x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x =
26 ndmfv ¬ x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x =
27 25 26 eqtr4d ¬ x dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x
28 16 27 pm2.61i 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F V dom 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F × x = 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x
29 funpartfv 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F x = F x
30 5 28 29 3eqtri 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F x = F x
31 3 30 vtoclg A V 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A = F A
32 fvprc ¬ A V 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A =
33 fvprc ¬ A V F A =
34 32 33 eqtr4d ¬ A V 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A = F A
35 31 34 pm2.61i 𝖥𝗎𝗅𝗅𝖥𝗎𝗇 F A = F A