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

Metamath Proof Explorer

Theorem fsuppcurry1

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

Ref Expression
Hypotheses fsuppcurry1.g 
|- G = ( x e. B |-> ( C F x ) )
fsuppcurry1.z 
|- ( ph -> Z e. U )
fsuppcurry1.a 
|- ( ph -> A e. V )
fsuppcurry1.b 
|- ( ph -> B e. W )
fsuppcurry1.f 
|- ( ph -> F Fn ( A X. B ) )
fsuppcurry1.c 
|- ( ph -> C e. A )
fsuppcurry1.1 
|- ( ph -> F finSupp Z )
Assertion fsuppcurry1 
|- ( ph -> G finSupp Z )

Proof

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