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 30142
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 7026 . . . . 5 (𝑥 = 𝑦 → (𝑥𝐹𝐶) = (𝑦𝐹𝐶))
32cbvmptv 5064 . . . 4 (𝑥𝐴 ↦ (𝑥𝐹𝐶)) = (𝑦𝐴 ↦ (𝑦𝐹𝐶))
41, 3eqtri 2818 . . 3 𝐺 = (𝑦𝐴 ↦ (𝑦𝐹𝐶))
5 fsuppcurry2.a . . . 4 (𝜑𝐴𝑉)
65mptexd 6856 . . 3 (𝜑 → (𝑦𝐴 ↦ (𝑦𝐹𝐶)) ∈ V)
74, 6syl5eqel 2886 . 2 (𝜑𝐺 ∈ V)
81funmpt2 6267 . . 3 Fun 𝐺
98a1i 11 . 2 (𝜑 → Fun 𝐺)
10 fsuppcurry2.z . 2 (𝜑𝑍𝑈)
11 fo1st 7568 . . . . 5 1st :V–onto→V
12 fofun 6462 . . . . 5 (1st :V–onto→V → Fun 1st )
1311, 12ax-mp 5 . . . 4 Fun 1st
14 funres 6270 . . . 4 (Fun 1st → Fun (1st ↾ (V × V)))
1513, 14mp1i 13 . . 3 (𝜑 → Fun (1st ↾ (V × V)))
16 fsuppcurry2.1 . . . 4 (𝜑𝐹 finSupp 𝑍)
1716fsuppimpd 8689 . . 3 (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
18 imafi 8666 . . 3 ((Fun (1st ↾ (V × V)) ∧ (𝐹 supp 𝑍) ∈ Fin) → ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin)
1915, 17, 18syl2anc 584 . 2 (𝜑 → ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin)
20 ovexd 7053 . . . 4 ((𝜑𝑦𝐴) → (𝑦𝐹𝐶) ∈ V)
2120, 4fmptd 6744 . . 3 (𝜑𝐺:𝐴⟶V)
22 eldif 3871 . . . 4 (𝑦 ∈ (𝐴 ∖ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍))) ↔ (𝑦𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍))))
23 simplr 765 . . . . . . . . . . 11 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝑦𝐴)
24 fsuppcurry2.c . . . . . . . . . . . 12 (𝜑𝐶𝐵)
2524ad2antrr 722 . . . . . . . . . . 11 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝐶𝐵)
2623, 25opelxpd 5484 . . . . . . . . . 10 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵))
27 df-ov 7022 . . . . . . . . . . 11 (𝑦𝐹𝐶) = (𝐹‘⟨𝑦, 𝐶⟩)
28 ovexd 7053 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦𝐹𝐶) ∈ V)
291, 2, 23, 28fvmptd3 6660 . . . . . . . . . . . 12 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐺𝑦) = (𝑦𝐹𝐶))
30 simpr 485 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ¬ (𝐺𝑦) = 𝑍)
3130neqned 2990 . . . . . . . . . . . 12 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐺𝑦) ≠ 𝑍)
3229, 31eqnetrrd 3051 . . . . . . . . . . 11 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦𝐹𝐶) ≠ 𝑍)
3327, 32syl5eqner 3058 . . . . . . . . . 10 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐹‘⟨𝑦, 𝐶⟩) ≠ 𝑍)
34 fsuppcurry2.f . . . . . . . . . . . 12 (𝜑𝐹 Fn (𝐴 × 𝐵))
35 fsuppcurry2.b . . . . . . . . . . . . 13 (𝜑𝐵𝑊)
365, 35xpexd 7334 . . . . . . . . . . . 12 (𝜑 → (𝐴 × 𝐵) ∈ V)
37 elsuppfn 7692 . . . . . . . . . . . 12 ((𝐹 Fn (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝑍𝑈) → (⟨𝑦, 𝐶⟩ ∈ (𝐹 supp 𝑍) ↔ (⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵) ∧ (𝐹‘⟨𝑦, 𝐶⟩) ≠ 𝑍)))
3834, 36, 10, 37syl3anc 1364 . . . . . . . . . . 11 (𝜑 → (⟨𝑦, 𝐶⟩ ∈ (𝐹 supp 𝑍) ↔ (⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵) ∧ (𝐹‘⟨𝑦, 𝐶⟩) ≠ 𝑍)))
3938ad2antrr 722 . . . . . . . . . 10 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (⟨𝑦, 𝐶⟩ ∈ (𝐹 supp 𝑍) ↔ (⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵) ∧ (𝐹‘⟨𝑦, 𝐶⟩) ≠ 𝑍)))
4026, 33, 39mpbir2and 709 . . . . . . . . 9 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ⟨𝑦, 𝐶⟩ ∈ (𝐹 supp 𝑍))
41 simpr 485 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → 𝑧 = ⟨𝑦, 𝐶⟩)
4241fveq2d 6545 . . . . . . . . . 10 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ((1st ↾ (V × V))‘𝑧) = ((1st ↾ (V × V))‘⟨𝑦, 𝐶⟩))
43 xpss 5462 . . . . . . . . . . . 12 (𝐴 × 𝐵) ⊆ (V × V)
4426adantr 481 . . . . . . . . . . . 12 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵))
4543, 44sseldi 3889 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ⟨𝑦, 𝐶⟩ ∈ (V × V))
4645fvresd 6561 . . . . . . . . . 10 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ((1st ↾ (V × V))‘⟨𝑦, 𝐶⟩) = (1st ‘⟨𝑦, 𝐶⟩))
4723adantr 481 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → 𝑦𝐴)
4825adantr 481 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → 𝐶𝐵)
49 op1stg 7560 . . . . . . . . . . 11 ((𝑦𝐴𝐶𝐵) → (1st ‘⟨𝑦, 𝐶⟩) = 𝑦)
5047, 48, 49syl2anc 584 . . . . . . . . . 10 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → (1st ‘⟨𝑦, 𝐶⟩) = 𝑦)
5142, 46, 503eqtrd 2834 . . . . . . . . 9 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ((1st ↾ (V × V))‘𝑧) = 𝑦)
5240, 51rspcedeq1vd 3566 . . . . . . . 8 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V × V))‘𝑧) = 𝑦)
53 fofn 6463 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st Fn V)
54 fnresin 30053 . . . . . . . . . . . . 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 3914 . . . . . . . . . . . . . 14 (V × V) ⊆ V
57 sseqin2 4114 . . . . . . . . . . . . . 14 ((V × V) ⊆ V ↔ (V ∩ (V × V)) = (V × V))
5856, 57mpbi 231 . . . . . . . . . . . . 13 (V ∩ (V × V)) = (V × V)
5958fneq2i 6324 . . . . . . . . . . . 12 ((1st ↾ (V × V)) Fn (V ∩ (V × V)) ↔ (1st ↾ (V × V)) Fn (V × V))
6055, 59mpbi 231 . . . . . . . . . . 11 (1st ↾ (V × V)) Fn (V × V)
6160a1i 11 . . . . . . . . . 10 (𝜑 → (1st ↾ (V × V)) Fn (V × V))
62 suppssdm 7697 . . . . . . . . . . . 12 (𝐹 supp 𝑍) ⊆ dom 𝐹
6334fndmd 6329 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = (𝐴 × 𝐵))
6462, 63sseqtrid 3942 . . . . . . . . . . 11 (𝜑 → (𝐹 supp 𝑍) ⊆ (𝐴 × 𝐵))
6564, 43syl6ss 3903 . . . . . . . . . 10 (𝜑 → (𝐹 supp 𝑍) ⊆ (V × V))
6661, 65fvelimabd 6609 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V × V))‘𝑧) = 𝑦))
6766ad2antrr 722 . . . . . . . 8 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V × V))‘𝑧) = 𝑦))
6852, 67mpbird 258 . . . . . . 7 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))
6968ex 413 . . . . . 6 ((𝜑𝑦𝐴) → (¬ (𝐺𝑦) = 𝑍𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍))))
7069con1d 147 . . . . 5 ((𝜑𝑦𝐴) → (¬ 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) → (𝐺𝑦) = 𝑍))
7170impr 455 . . . 4 ((𝜑 ∧ (𝑦𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))) → (𝐺𝑦) = 𝑍)
7222, 71sylan2b 593 . . 3 ((𝜑𝑦 ∈ (𝐴 ∖ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))) → (𝐺𝑦) = 𝑍)
7321, 72suppss 7714 . 2 (𝜑 → (𝐺 supp 𝑍) ⊆ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))
74 suppssfifsupp 8697 . 2 (((𝐺 ∈ V ∧ Fun 𝐺𝑍𝑈) ∧ (((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))) → 𝐺 finSupp 𝑍)
757, 9, 10, 19, 73, 74syl32anc 1371 1 (𝜑𝐺 finSupp 𝑍)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396   = wceq 1522  wcel 2080  wne 2983  wrex 3105  Vcvv 3436  cdif 3858  cin 3860  wss 3861  cop 4480   class class class wbr 4964  cmpt 5043   × cxp 5444  dom cdm 5446  cres 5448  cima 5449  Fun wfun 6222   Fn wfn 6223  ontowfo 6226  cfv 6228  (class class class)co 7019  1st c1st 7546   supp csupp 7684  Fincfn 8360   finSupp cfsupp 8682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-13 2343  ax-ext 2768  ax-rep 5084  ax-sep 5097  ax-nul 5104  ax-pow 5160  ax-pr 5224  ax-un 7322
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-mo 2575  df-eu 2611  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-ne 2984  df-ral 3109  df-rex 3110  df-reu 3111  df-rab 3113  df-v 3438  df-sbc 3708  df-csb 3814  df-dif 3864  df-un 3866  df-in 3868  df-ss 3876  df-pss 3878  df-nul 4214  df-if 4384  df-pw 4457  df-sn 4475  df-pr 4477  df-tp 4479  df-op 4481  df-uni 4748  df-iun 4829  df-br 4965  df-opab 5027  df-mpt 5044  df-tr 5067  df-id 5351  df-eprel 5356  df-po 5365  df-so 5366  df-fr 5405  df-we 5407  df-xp 5452  df-rel 5453  df-cnv 5454  df-co 5455  df-dm 5456  df-rn 5457  df-res 5458  df-ima 5459  df-ord 6072  df-on 6073  df-lim 6074  df-suc 6075  df-iota 6192  df-fun 6230  df-fn 6231  df-f 6232  df-f1 6233  df-fo 6234  df-f1o 6235  df-fv 6236  df-ov 7022  df-oprab 7023  df-mpo 7024  df-om 7440  df-1st 7548  df-supp 7685  df-1o 7956  df-er 8142  df-en 8361  df-dom 8362  df-fin 8364  df-fsupp 8683
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator