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 32548
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 7420 . . . . 5 (š‘„ = š‘¦ → (š‘„š¹š¶) = (š‘¦š¹š¶))
32cbvmptv 5257 . . . 4 (š‘„ ∈ š“ ↦ (š‘„š¹š¶)) = (š‘¦ ∈ š“ ↦ (š‘¦š¹š¶))
41, 3eqtri 2753 . . 3 šŗ = (š‘¦ ∈ š“ ↦ (š‘¦š¹š¶))
5 fsuppcurry2.a . . . 4 (šœ‘ → š“ ∈ š‘‰)
65mptexd 7230 . . 3 (šœ‘ → (š‘¦ ∈ š“ ↦ (š‘¦š¹š¶)) ∈ V)
74, 6eqeltrid 2829 . 2 (šœ‘ → šŗ ∈ V)
81funmpt2 6587 . . 3 Fun šŗ
98a1i 11 . 2 (šœ‘ → Fun šŗ)
10 fsuppcurry2.z . 2 (šœ‘ → š‘ ∈ š‘ˆ)
11 fo1st 8007 . . . . 5 1st :V–onto→V
12 fofun 6805 . . . . 5 (1st :V–onto→V → Fun 1st )
1311, 12ax-mp 5 . . . 4 Fun 1st
14 funres 6590 . . . 4 (Fun 1st → Fun (1st ↾ (V Ɨ V)))
1513, 14mp1i 13 . . 3 (šœ‘ → Fun (1st ↾ (V Ɨ V)))
16 fsuppcurry2.1 . . . 4 (šœ‘ → š¹ finSupp š‘)
1716fsuppimpd 9388 . . 3 (šœ‘ → (š¹ supp š‘) ∈ Fin)
18 imafi 9193 . . 3 ((Fun (1st ↾ (V Ɨ V)) ∧ (š¹ supp š‘) ∈ Fin) → ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ∈ Fin)
1915, 17, 18syl2anc 582 . 2 (šœ‘ → ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ∈ Fin)
20 ovexd 7448 . . . 4 ((šœ‘ ∧ š‘¦ ∈ š“) → (š‘¦š¹š¶) ∈ V)
2120, 4fmptd 7117 . . 3 (šœ‘ → šŗ:š“āŸ¶V)
22 eldif 3951 . . . 4 (š‘¦ ∈ (š“ āˆ– ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘))) ↔ (š‘¦ ∈ š“ ∧ ¬ š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘))))
23 simplr 767 . . . . . . . . . . 11 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → š‘¦ ∈ š“)
24 fsuppcurry2.c . . . . . . . . . . . 12 (šœ‘ → š¶ ∈ šµ)
2524ad2antrr 724 . . . . . . . . . . 11 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → š¶ ∈ šµ)
2623, 25opelxpd 5712 . . . . . . . . . 10 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ))
27 df-ov 7416 . . . . . . . . . . 11 (š‘¦š¹š¶) = (š¹ā€˜āŸØš‘¦, š¶āŸ©)
28 ovexd 7448 . . . . . . . . . . . . 13 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š‘¦š¹š¶) ∈ V)
291, 2, 23, 28fvmptd3 7021 . . . . . . . . . . . 12 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (šŗā€˜š‘¦) = (š‘¦š¹š¶))
30 simpr 483 . . . . . . . . . . . . 13 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → ¬ (šŗā€˜š‘¦) = š‘)
3130neqned 2937 . . . . . . . . . . . 12 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (šŗā€˜š‘¦) ≠ š‘)
3229, 31eqnetrrd 2999 . . . . . . . . . . 11 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š‘¦š¹š¶) ≠ š‘)
3327, 32eqnetrrid 3006 . . . . . . . . . 10 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)
34 fsuppcurry2.f . . . . . . . . . . . 12 (šœ‘ → š¹ Fn (š“ Ɨ šµ))
35 fsuppcurry2.b . . . . . . . . . . . . 13 (šœ‘ → šµ ∈ š‘Š)
365, 35xpexd 7748 . . . . . . . . . . . 12 (šœ‘ → (š“ Ɨ šµ) ∈ V)
37 elsuppfn 8168 . . . . . . . . . . . 12 ((š¹ Fn (š“ Ɨ šµ) ∧ (š“ Ɨ šµ) ∈ V ∧ š‘ ∈ š‘ˆ) → (āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘) ↔ (āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ) ∧ (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)))
3834, 36, 10, 37syl3anc 1368 . . . . . . . . . . 11 (šœ‘ → (āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘) ↔ (āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ) ∧ (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)))
3938ad2antrr 724 . . . . . . . . . 10 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘) ↔ (āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ) ∧ (š¹ā€˜āŸØš‘¦, š¶āŸ©) ≠ š‘)))
4026, 33, 39mpbir2and 711 . . . . . . . . 9 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → āŸØš‘¦, š¶āŸ© ∈ (š¹ supp š‘))
41 simpr 483 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → š‘§ = āŸØš‘¦, š¶āŸ©)
4241fveq2d 6894 . . . . . . . . . 10 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → ((1st ↾ (V Ɨ V))ā€˜š‘§) = ((1st ↾ (V Ɨ V))ā€˜āŸØš‘¦, š¶āŸ©))
43 xpss 5689 . . . . . . . . . . . 12 (š“ Ɨ šµ) āŠ† (V Ɨ V)
4426adantr 479 . . . . . . . . . . . 12 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → āŸØš‘¦, š¶āŸ© ∈ (š“ Ɨ šµ))
4543, 44sselid 3971 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → āŸØš‘¦, š¶āŸ© ∈ (V Ɨ V))
4645fvresd 6910 . . . . . . . . . 10 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → ((1st ↾ (V Ɨ V))ā€˜āŸØš‘¦, š¶āŸ©) = (1st ā€˜āŸØš‘¦, š¶āŸ©))
4723adantr 479 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → š‘¦ ∈ š“)
4825adantr 479 . . . . . . . . . . 11 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → š¶ ∈ šµ)
49 op1stg 7999 . . . . . . . . . . 11 ((š‘¦ ∈ š“ ∧ š¶ ∈ šµ) → (1st ā€˜āŸØš‘¦, š¶āŸ©) = š‘¦)
5047, 48, 49syl2anc 582 . . . . . . . . . 10 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → (1st ā€˜āŸØš‘¦, š¶āŸ©) = š‘¦)
5142, 46, 503eqtrd 2769 . . . . . . . . 9 ((((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) ∧ š‘§ = āŸØš‘¦, š¶āŸ©) → ((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦)
5240, 51rspcedeq1vd 3610 . . . . . . . 8 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → āˆƒš‘§ ∈ (š¹ supp š‘)((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦)
53 fofn 6806 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st Fn V)
54 fnresin 32451 . . . . . . . . . . . . 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 3998 . . . . . . . . . . . . . 14 (V Ɨ V) āŠ† V
57 sseqin2 4210 . . . . . . . . . . . . . 14 ((V Ɨ V) āŠ† V ↔ (V ∩ (V Ɨ V)) = (V Ɨ V))
5856, 57mpbi 229 . . . . . . . . . . . . 13 (V ∩ (V Ɨ V)) = (V Ɨ V)
5958fneq2i 6647 . . . . . . . . . . . 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 8175 . . . . . . . . . . . 12 (š¹ supp š‘) āŠ† dom š¹
6334fndmd 6654 . . . . . . . . . . . 12 (šœ‘ → dom š¹ = (š“ Ɨ šµ))
6462, 63sseqtrid 4026 . . . . . . . . . . 11 (šœ‘ → (š¹ supp š‘) āŠ† (š“ Ɨ šµ))
6564, 43sstrdi 3986 . . . . . . . . . 10 (šœ‘ → (š¹ supp š‘) āŠ† (V Ɨ V))
6661, 65fvelimabd 6965 . . . . . . . . 9 (šœ‘ → (š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ↔ āˆƒš‘§ ∈ (š¹ supp š‘)((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦))
6766ad2antrr 724 . . . . . . . 8 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → (š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ↔ āˆƒš‘§ ∈ (š¹ supp š‘)((1st ↾ (V Ɨ V))ā€˜š‘§) = š‘¦))
6852, 67mpbird 256 . . . . . . 7 (((šœ‘ ∧ š‘¦ ∈ š“) ∧ ¬ (šŗā€˜š‘¦) = š‘) → š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))
6968ex 411 . . . . . 6 ((šœ‘ ∧ š‘¦ ∈ š“) → (¬ (šŗā€˜š‘¦) = š‘ → š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘))))
7069con1d 145 . . . . 5 ((šœ‘ ∧ š‘¦ ∈ š“) → (¬ š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) → (šŗā€˜š‘¦) = š‘))
7170impr 453 . . . 4 ((šœ‘ ∧ (š‘¦ ∈ š“ ∧ ¬ š‘¦ ∈ ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))) → (šŗā€˜š‘¦) = š‘)
7222, 71sylan2b 592 . . 3 ((šœ‘ ∧ š‘¦ ∈ (š“ āˆ– ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))) → (šŗā€˜š‘¦) = š‘)
7321, 72suppss 8192 . 2 (šœ‘ → (šŗ supp š‘) āŠ† ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))
74 suppssfifsupp 9398 . 2 (((šŗ ∈ V ∧ Fun šŗ ∧ š‘ ∈ š‘ˆ) ∧ (((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)) ∈ Fin ∧ (šŗ supp š‘) āŠ† ((1st ↾ (V Ɨ V)) ā€œ (š¹ supp š‘)))) → šŗ finSupp š‘)
757, 9, 10, 19, 73, 74syl32anc 1375 1 (šœ‘ → šŗ finSupp š‘)
Colors of variables: wff setvar class
Syntax hints:  Ā¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098   ≠ wne 2930  āˆƒwrex 3060  Vcvv 3463   āˆ– cdif 3938   ∩ cin 3940   āŠ† wss 3941  āŸØcop 4631   class class class wbr 5144   ↦ cmpt 5227   Ɨ cxp 5671  dom cdm 5673   ↾ cres 5675   ā€œ cima 5676  Fun wfun 6537   Fn wfn 6538  ā€“onto→wfo 6541  ā€˜cfv 6543  (class class class)co 7413  1st c1st 7985   supp csupp 8158  Fincfn 8957   finSupp cfsupp 9380
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5281  ax-sep 5295  ax-nul 5302  ax-pow 5360  ax-pr 5424  ax-un 7735
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3961  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5145  df-opab 5207  df-mpt 5228  df-tr 5262  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7987  df-supp 8159  df-1o 8480  df-en 8958  df-fin 8961  df-fsupp 9381
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator