Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fsuppcurry2 Structured version   Visualization version   GIF version

Theorem fsuppcurry2 32479
Description: Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023.)
Hypotheses
Ref Expression
fsuppcurry2.g šŗ = (š‘„ ∈ š“ ↦ (š‘„š¹š¶))
fsuppcurry2.z (šœ‘ → š‘ ∈ š‘ˆ)
fsuppcurry2.a (šœ‘ → š“ ∈ š‘‰)
fsuppcurry2.b (šœ‘ → šµ ∈ š‘Š)
fsuppcurry2.f (šœ‘ → š¹ Fn (š“ Ɨ šµ))
fsuppcurry2.c (šœ‘ → š¶ ∈ šµ)
fsuppcurry2.1 (šœ‘ → š¹ finSupp š‘)
Assertion
Ref Expression
fsuppcurry2 (šœ‘ → šŗ finSupp š‘)
Distinct variable groups:   š‘„,š“   š‘„,š¶   š‘„,š¹
Allowed substitution hints:   šœ‘(š‘„)   šµ(š‘„)   š‘ˆ(š‘„)   šŗ(š‘„)   š‘‰(š‘„)   š‘Š(š‘„)   š‘(š‘„)

Proof of Theorem fsuppcurry2
Dummy variables š‘¦ š‘§ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsuppcurry2.g . . . 4 šŗ = (š‘„ ∈ š“ ↦ (š‘„š¹š¶))
2 oveq1 7421 . . . . 5 (š‘„ = š‘¦ → (š‘„š¹š¶) = (š‘¦š¹š¶))
32cbvmptv 5255 . . . 4 (š‘„ ∈ š“ ↦ (š‘„š¹š¶)) = (š‘¦ ∈ š“ ↦ (š‘¦š¹š¶))
41, 3eqtri 2755 . . 3 šŗ = (š‘¦ ∈ š“ ↦ (š‘¦š¹š¶))
5 fsuppcurry2.a . . . 4 (šœ‘ → š“ ∈ š‘‰)
65mptexd 7230 . . 3 (šœ‘ → (š‘¦ ∈ š“ ↦ (š‘¦š¹š¶)) ∈ V)
74, 6eqeltrid 2832 . 2 (šœ‘ → šŗ ∈ V)
81funmpt2 6586 . . 3 Fun šŗ
98a1i 11 . 2 (šœ‘ → Fun šŗ)
10 fsuppcurry2.z . 2 (šœ‘ → š‘ ∈ š‘ˆ)
11 fo1st 8005 . . . . 5 1st :V–onto→V
12 fofun 6806 . . . . 5 (1st :V–onto→V → Fun 1st )
1311, 12ax-mp 5 . . . 4 Fun 1st
14 funres 6589 . . . 4 (Fun 1st → Fun (1st ↾ (V Ɨ V)))
1513, 14mp1i 13 . . 3 (šœ‘ → Fun (1st ↾ (V Ɨ V)))
16 fsuppcurry2.1 . . . 4 (šœ‘ → š¹ finSupp š‘)
1716fsuppimpd 9383 . . 3 (šœ‘ → (š¹ supp š‘) ∈ Fin)
18 imafi 9189 . . 3 ((Fun (1st ↾ (V Ɨ V)) ∧ (š¹ supp š‘) ∈ Fin) → ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ∈ Fin)
1915, 17, 18syl2anc 583 . 2 (šœ‘ → ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ∈ Fin)
20 ovexd 7449 . . . 4 ((šœ‘ ∧ š‘¦ ∈ š“) → (š‘¦š¹š¶) ∈ V)
2120, 4fmptd 7118 . . 3 (šœ‘ → šŗ:š“āŸ¶V)
22 eldif 3954 . . . 4 (š‘¦ ∈ (š“ āˆ– ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘))) ↔ (š‘¦ ∈ š“ ∧ ¬ š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘))))
23 simplr 768 . . . . . . . . . . 11 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → š‘¦ ∈ š“)
24 fsuppcurry2.c . . . . . . . . . . . 12 (šœ‘ → š¶ ∈ šµ)
2524ad2antrr 725 . . . . . . . . . . 11 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → š¶ ∈ šµ)
2623, 25opelxpd 5711 . . . . . . . . . 10 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ))
27 df-ov 7417 . . . . . . . . . . 11 (š‘¦š¹š¶) = (š¹ā€˜āŸØš‘¦, š¶āŸ©)
28 ovexd 7449 . . . . . . . . . . . . 13 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š‘¦š¹š¶) ∈ V)
291, 2, 23, 28fvmptd3 7022 . . . . . . . . . . . 12 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (šŗā€˜š‘¦) = (š‘¦š¹š¶))
30 simpr 484 . . . . . . . . . . . . 13 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → ¬ (šŗā€˜š‘¦) = š‘)
3130neqned 2942 . . . . . . . . . . . 12 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (šŗā€˜š‘¦) ≠ š‘)
3229, 31eqnetrrd 3004 . . . . . . . . . . 11 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š‘¦š¹š¶) ≠ š‘)
3327, 32eqnetrrid 3011 . . . . . . . . . 10 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)
34 fsuppcurry2.f . . . . . . . . . . . 12 (šœ‘ → š¹ Fn (š“ Ɨ šµ))
35 fsuppcurry2.b . . . . . . . . . . . . 13 (šœ‘ → šµ ∈ š‘Š)
365, 35xpexd 7745 . . . . . . . . . . . 12 (šœ‘ → (š“ Ɨ šµ) ∈ V)
37 elsuppfn 8167 . . . . . . . . . . . 12 ((š¹ Fn (š“ Ɨ šµ) ∧ (š“ Ɨ šµ) ∈ V ∧ š‘ ∈ š‘ˆ) → (āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘) ↔ (āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ) ∧ (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)))
3834, 36, 10, 37syl3anc 1369 . . . . . . . . . . 11 (šœ‘ → (āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘) ↔ (āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ) ∧ (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)))
3938ad2antrr 725 . . . . . . . . . 10 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘) ↔ (āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ) ∧ (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)))
4026, 33, 39mpbir2and 712 . . . . . . . . 9 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘))
41 simpr 484 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → š‘§ = āŸØš‘¦, š¶āŸ©)
4241fveq2d 6895 . . . . . . . . . 10 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → ((1st ↾ (V Ɨ V))ā€˜š‘§) = ((1st ↾ (V Ɨ V))ā€˜āŸØš‘¦, š¶āŸ©))
43 xpss 5688 . . . . . . . . . . . 12 (š“ Ɨ šµ) āŠ† (V Ɨ V)
4426adantr 480 . . . . . . . . . . . 12 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ))
4543, 44sselid 3976 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → āŸØš‘¦, š¶āŸ© ∈ (V Ɨ V))
4645fvresd 6911 . . . . . . . . . 10 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → ((1st ↾ (V Ɨ V))ā€˜āŸØš‘¦, š¶āŸ©) = (1st ā€˜āŸØš‘¦, š¶āŸ©))
4723adantr 480 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → š‘¦ ∈ š“)
4825adantr 480 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → š¶ ∈ šµ)
49 op1stg 7997 . . . . . . . . . . 11 ((š‘¦ ∈ š“ ∧ š¶ ∈ šµ) → (1st ā€˜āŸØš‘¦, š¶āŸ©) = š‘¦)
5047, 48, 49syl2anc 583 . . . . . . . . . 10 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → (1st ā€˜āŸØš‘¦, š¶āŸ©) = š‘¦)
5142, 46, 503eqtrd 2771 . . . . . . . . 9 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → ((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦)
5240, 51rspcedeq1vd 3614 . . . . . . . 8 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → āˆƒš‘§ ∈ (š¹ supp š‘)((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦)
53 fofn 6807 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st Fn V)
54 fnresin 32381 . . . . . . . . . . . . 13 (1st Fn V → (1st ↾ (V Ɨ V)) Fn (V ∩ (V Ɨ V)))
5511, 53, 54mp2b 10 . . . . . . . . . . . 12 (1st ↾ (V Ɨ V)) Fn (V ∩ (V Ɨ V))
56 ssv 4002 . . . . . . . . . . . . . 14 (V Ɨ V) āŠ† V
57 sseqin2 4211 . . . . . . . . . . . . . 14 ((V Ɨ V) āŠ† V ↔ (V ∩ (V Ɨ V)) = (V Ɨ V))
5856, 57mpbi 229 . . . . . . . . . . . . 13 (V ∩ (V Ɨ V)) = (V Ɨ V)
5958fneq2i 6646 . . . . . . . . . . . 12 ((1st ↾ (V Ɨ V)) Fn (V ∩ (V Ɨ V)) ↔ (1st ↾ (V Ɨ V)) Fn (V Ɨ V))
6055, 59mpbi 229 . . . . . . . . . . 11 (1st ↾ (V Ɨ V)) Fn (V Ɨ V)
6160a1i 11 . . . . . . . . . 10 (šœ‘ → (1st ↾ (V Ɨ V)) Fn (V Ɨ V))
62 suppssdm 8173 . . . . . . . . . . . 12 (š¹ supp š‘) āŠ† dom š¹
6334fndmd 6653 . . . . . . . . . . . 12 (šœ‘ → dom š¹ = (š“ Ɨ šµ))
6462, 63sseqtrid 4030 . . . . . . . . . . 11 (šœ‘ → (š¹ supp š‘) āŠ† (š“ Ɨ šµ))
6564, 43sstrdi 3990 . . . . . . . . . 10 (šœ‘ → (š¹ supp š‘) āŠ† (V Ɨ V))
6661, 65fvelimabd 6966 . . . . . . . . 9 (šœ‘ → (š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ↔ āˆƒš‘§ ∈ (š¹ supp š‘)((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦))
6766ad2antrr 725 . . . . . . . 8 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ↔ āˆƒš‘§ ∈ (š¹ supp š‘)((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦))
6852, 67mpbird 257 . . . . . . 7 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))
6968ex 412 . . . . . 6 ((šœ‘ ∧ š‘¦ ∈ š“) → (¬ (šŗā€˜š‘¦) = š‘ → š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘))))
7069con1d 145 . . . . 5 ((šœ‘ ∧ š‘¦ ∈ š“) → (¬ š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) → (šŗā€˜š‘¦) = š‘))
7170impr 454 . . . 4 ((šœ‘ ∧ (š‘¦ ∈ š“ ∧ ¬ š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))) → (šŗā€˜š‘¦) = š‘)
7222, 71sylan2b 593 . . 3 ((šœ‘ ∧ š‘¦ ∈ (š“ āˆ– ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))) → (šŗā€˜š‘¦) = š‘)
7321, 72suppss 8190 . 2 (šœ‘ → (šŗ supp š‘) āŠ† ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))
74 suppssfifsupp 9392 . 2 (((šŗ ∈ V ∧ Fun šŗ ∧ š‘ ∈ š‘ˆ) ∧ (((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ∈ Fin ∧ (šŗ supp š‘) āŠ† ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))) → šŗ finSupp š‘)
757, 9, 10, 19, 73, 74syl32anc 1376 1 (šœ‘ → šŗ finSupp š‘)
Colors of variables: wff setvar class
Syntax hints:  Ā¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1534   ∈ wcel 2099   ≠ wne 2935  āˆƒwrex 3065  Vcvv 3469   āˆ– cdif 3941   ∩ cin 3943   āŠ† wss 3944  āŸØcop 4630   class class class wbr 5142   ↦ cmpt 5225   Ɨ cxp 5670  dom cdm 5672   ↾ cres 5674   ā€œ cima 5675  Fun wfun 6536   Fn wfn 6537  ā€“onto→wfo 6540  ā€˜cfv 6542  (class class class)co 7414  1st c1st 7983   supp csupp 8157  Fincfn 8953   finSupp cfsupp 9375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7732
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-ral 3057  df-rex 3066  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-iun 4993  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-om 7863  df-1st 7985  df-supp 8158  df-1o 8478  df-en 8954  df-fin 8957  df-fsupp 9376
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator