Metamath Proof Explorer


Theorem funpartfun

Description: The functional part of F is a function. (Contributed by Scott Fenton, 16-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion funpartfun Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F

Proof

Step Hyp Ref Expression
1 relres Rel F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
2 vex z V
3 2 brresi x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z x dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 x F z
4 3 simprbi x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z x F z
5 vex y V
6 5 brresi x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 x F y
7 funpartlem x dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 w F x = w
8 7 anbi1i x dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 x F y w F x = w x F y
9 6 8 bitri x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y w F x = w x F y
10 df-br x F y x y F
11 df-br x F z x z F
12 10 11 anbi12i x F y x F z x y F x z F
13 vex x V
14 13 5 elimasn y F x x y F
15 13 2 elimasn z F x x z F
16 14 15 anbi12i y F x z F x x y F x z F
17 12 16 bitr4i x F y x F z y F x z F x
18 eleq2 F x = w y F x y w
19 eleq2 F x = w z F x z w
20 18 19 anbi12d F x = w y F x z F x y w z w
21 velsn y w y = w
22 velsn z w z = w
23 equtr2 y = w z = w y = z
24 21 22 23 syl2anb y w z w y = z
25 20 24 syl6bi F x = w y F x z F x y = z
26 17 25 syl5bi F x = w x F y x F z y = z
27 26 exlimiv w F x = w x F y x F z y = z
28 27 impl w F x = w x F y x F z y = z
29 9 28 sylanb x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x F z y = z
30 4 29 sylan2 x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z y = z
31 30 gen2 y z x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z y = z
32 31 ax-gen x y z x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z y = z
33 df-funpart 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F = F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
34 33 funeqi Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Fun F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌
35 dffun2 Fun F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 Rel F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 x y z x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z y = z
36 34 35 bitri Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F Rel F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 x y z x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 y x F dom 𝖨𝗆𝖺𝗀𝖾 F 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 V × 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇𝗌 z y = z
37 1 32 36 mpbir2an Fun 𝖥𝗎𝗇𝖯𝖺𝗋𝗍 F