Metamath Proof Explorer


Theorem fsuppcurry2

Description: Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023)

Ref Expression
Hypotheses fsuppcurry2.g G = x A x F C
fsuppcurry2.z φ Z U
fsuppcurry2.a φ A V
fsuppcurry2.b φ B W
fsuppcurry2.f φ F Fn A × B
fsuppcurry2.c φ C B
fsuppcurry2.1 φ finSupp Z F
Assertion fsuppcurry2 φ finSupp Z G

Proof

Step Hyp Ref Expression
1 fsuppcurry2.g G = x A x F C
2 fsuppcurry2.z φ Z U
3 fsuppcurry2.a φ A V
4 fsuppcurry2.b φ B W
5 fsuppcurry2.f φ F Fn A × B
6 fsuppcurry2.c φ C B
7 fsuppcurry2.1 φ finSupp Z F
8 oveq1 x = y x F C = y F C
9 8 cbvmptv x A x F C = y A y F C
10 1 9 eqtri G = y A y F C
11 3 mptexd φ y A y F C V
12 10 11 eqeltrid φ G V
13 1 funmpt2 Fun G
14 13 a1i φ Fun G
15 fo1st 1 st : V onto V
16 fofun 1 st : V onto V Fun 1 st
17 15 16 ax-mp Fun 1 st
18 funres Fun 1 st Fun 1 st V × V
19 17 18 mp1i φ Fun 1 st V × V
20 7 fsuppimpd φ F supp Z Fin
21 imafi Fun 1 st V × V F supp Z Fin 1 st V × V F supp Z Fin
22 19 20 21 syl2anc φ 1 st V × V F supp Z Fin
23 ovexd φ y A y F C V
24 23 10 fmptd φ G : A V
25 eldif y A 1 st V × V F supp Z y A ¬ y 1 st V × V F supp Z
26 simplr φ y A ¬ G y = Z y A
27 6 ad2antrr φ y A ¬ G y = Z C B
28 26 27 opelxpd φ y A ¬ G y = Z y C A × B
29 df-ov y F C = F y C
30 ovexd φ y A ¬ G y = Z y F C V
31 1 8 26 30 fvmptd3 φ y A ¬ G y = Z G y = y F C
32 simpr φ y A ¬ G y = Z ¬ G y = Z
33 32 neqned φ y A ¬ G y = Z G y Z
34 31 33 eqnetrrd φ y A ¬ G y = Z y F C Z
35 29 34 eqnetrrid φ y A ¬ G y = Z F y C Z
36 3 4 xpexd φ A × B V
37 elsuppfn F Fn A × B A × B V Z U y C supp Z F y C A × B F y C Z
38 5 36 2 37 syl3anc φ y C supp Z F y C A × B F y C Z
39 38 ad2antrr φ y A ¬ G y = Z y C supp Z F y C A × B F y C Z
40 28 35 39 mpbir2and φ y A ¬ G y = Z y C supp Z F
41 simpr φ y A ¬ G y = Z z = y C z = y C
42 41 fveq2d φ y A ¬ G y = Z z = y C 1 st V × V z = 1 st V × V y C
43 xpss A × B V × V
44 28 adantr φ y A ¬ G y = Z z = y C y C A × B
45 43 44 sselid φ y A ¬ G y = Z z = y C y C V × V
46 45 fvresd φ y A ¬ G y = Z z = y C 1 st V × V y C = 1 st y C
47 26 adantr φ y A ¬ G y = Z z = y C y A
48 27 adantr φ y A ¬ G y = Z z = y C C B
49 op1stg y A C B 1 st y C = y
50 47 48 49 syl2anc φ y A ¬ G y = Z z = y C 1 st y C = y
51 42 46 50 3eqtrd φ y A ¬ G y = Z z = y C 1 st V × V z = y
52 40 51 rspcedeq1vd φ y A ¬ G y = Z z supp Z F 1 st V × V z = y
53 fofn 1 st : V onto V 1 st Fn V
54 fnresin 1 st Fn V 1 st V × V Fn V V × V
55 15 53 54 mp2b 1 st V × V Fn V V × V
56 ssv V × V V
57 sseqin2 V × V V V V × V = V × V
58 56 57 mpbi V V × V = V × V
59 58 fneq2i 1 st V × V Fn V V × V 1 st V × V Fn V × V
60 55 59 mpbi 1 st V × V Fn V × V
61 60 a1i φ 1 st V × V Fn V × V
62 suppssdm F supp Z dom F
63 5 fndmd φ dom F = A × B
64 62 63 sseqtrid φ F supp Z A × B
65 64 43 sstrdi φ F supp Z V × V
66 61 65 fvelimabd φ y 1 st V × V F supp Z z supp Z F 1 st V × V z = y
67 66 ad2antrr φ y A ¬ G y = Z y 1 st V × V F supp Z z supp Z F 1 st V × V z = y
68 52 67 mpbird φ y A ¬ G y = Z y 1 st V × V F supp Z
69 68 ex φ y A ¬ G y = Z y 1 st V × V F supp Z
70 69 con1d φ y A ¬ y 1 st V × V F supp Z G y = Z
71 70 impr φ y A ¬ y 1 st V × V F supp Z G y = Z
72 25 71 sylan2b φ y A 1 st V × V F supp Z G y = Z
73 24 72 suppss φ G supp Z 1 st V × V F supp Z
74 suppssfifsupp G V Fun G Z U 1 st V × V F supp Z Fin G supp Z 1 st V × V F supp Z finSupp Z G
75 12 14 2 22 73 74 syl32anc φ finSupp Z G