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

Theorem fsuppcurry1 30501
 Description: Finite support of a curried function with a constant first argument. (Contributed by Thierry Arnoux, 7-Jul-2023.)
Hypotheses
Ref Expression
fsuppcurry1.g 𝐺 = (𝑥𝐵 ↦ (𝐶𝐹𝑥))
fsuppcurry1.z (𝜑𝑍𝑈)
fsuppcurry1.a (𝜑𝐴𝑉)
fsuppcurry1.b (𝜑𝐵𝑊)
fsuppcurry1.f (𝜑𝐹 Fn (𝐴 × 𝐵))
fsuppcurry1.c (𝜑𝐶𝐴)
fsuppcurry1.1 (𝜑𝐹 finSupp 𝑍)
Assertion
Ref Expression
fsuppcurry1 (𝜑𝐺 finSupp 𝑍)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐶   𝑥,𝐹
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)   𝑈(𝑥)   𝐺(𝑥)   𝑉(𝑥)   𝑊(𝑥)   𝑍(𝑥)

Proof of Theorem fsuppcurry1
Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fsuppcurry1.g . . . 4 𝐺 = (𝑥𝐵 ↦ (𝐶𝐹𝑥))
2 oveq2 7148 . . . . 5 (𝑥 = 𝑦 → (𝐶𝐹𝑥) = (𝐶𝐹𝑦))
32cbvmptv 5134 . . . 4 (𝑥𝐵 ↦ (𝐶𝐹𝑥)) = (𝑦𝐵 ↦ (𝐶𝐹𝑦))
41, 3eqtri 2821 . . 3 𝐺 = (𝑦𝐵 ↦ (𝐶𝐹𝑦))
5 fsuppcurry1.b . . . 4 (𝜑𝐵𝑊)
65mptexd 6969 . . 3 (𝜑 → (𝑦𝐵 ↦ (𝐶𝐹𝑦)) ∈ V)
74, 6eqeltrid 2894 . 2 (𝜑𝐺 ∈ V)
81funmpt2 6366 . . 3 Fun 𝐺
98a1i 11 . 2 (𝜑 → Fun 𝐺)
10 fsuppcurry1.z . 2 (𝜑𝑍𝑈)
11 fo2nd 7699 . . . . 5 2nd :V–onto→V
12 fofun 6569 . . . . 5 (2nd :V–onto→V → Fun 2nd )
1311, 12ax-mp 5 . . . 4 Fun 2nd
14 funres 6369 . . . 4 (Fun 2nd → Fun (2nd ↾ (V × V)))
1513, 14mp1i 13 . . 3 (𝜑 → Fun (2nd ↾ (V × V)))
16 fsuppcurry1.1 . . . 4 (𝜑𝐹 finSupp 𝑍)
1716fsuppimpd 8831 . . 3 (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
18 imafi 8808 . . 3 ((Fun (2nd ↾ (V × V)) ∧ (𝐹 supp 𝑍) ∈ Fin) → ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin)
1915, 17, 18syl2anc 587 . 2 (𝜑 → ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin)
20 ovexd 7175 . . . 4 ((𝜑𝑦𝐵) → (𝐶𝐹𝑦) ∈ V)
2120, 4fmptd 6860 . . 3 (𝜑𝐺:𝐵⟶V)
22 eldif 3891 . . . 4 (𝑦 ∈ (𝐵 ∖ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍))) ↔ (𝑦𝐵 ∧ ¬ 𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍))))
23 fsuppcurry1.c . . . . . . . . . . . 12 (𝜑𝐶𝐴)
2423ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝐶𝐴)
25 simplr 768 . . . . . . . . . . 11 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝑦𝐵)
2624, 25opelxpd 5558 . . . . . . . . . 10 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → ⟨𝐶, 𝑦⟩ ∈ (𝐴 × 𝐵))
27 df-ov 7143 . . . . . . . . . . 11 (𝐶𝐹𝑦) = (𝐹‘⟨𝐶, 𝑦⟩)
28 ovexd 7175 . . . . . . . . . . . . 13 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐶𝐹𝑦) ∈ V)
291, 2, 25, 28fvmptd3 6773 . . . . . . . . . . . 12 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐺𝑦) = (𝐶𝐹𝑦))
30 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → ¬ (𝐺𝑦) = 𝑍)
3130neqned 2994 . . . . . . . . . . . 12 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐺𝑦) ≠ 𝑍)
3229, 31eqnetrrd 3055 . . . . . . . . . . 11 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐶𝐹𝑦) ≠ 𝑍)
3327, 32eqnetrrid 3062 . . . . . . . . . 10 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐹‘⟨𝐶, 𝑦⟩) ≠ 𝑍)
34 fsuppcurry1.f . . . . . . . . . . . 12 (𝜑𝐹 Fn (𝐴 × 𝐵))
35 fsuppcurry1.a . . . . . . . . . . . . 13 (𝜑𝐴𝑉)
3635, 5xpexd 7461 . . . . . . . . . . . 12 (𝜑 → (𝐴 × 𝐵) ∈ V)
37 elsuppfn 7828 . . . . . . . . . . . 12 ((𝐹 Fn (𝐴 × 𝐵) ∧ (𝐴 × 𝐵) ∈ V ∧ 𝑍𝑈) → (⟨𝐶, 𝑦⟩ ∈ (𝐹 supp 𝑍) ↔ (⟨𝐶, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ (𝐹‘⟨𝐶, 𝑦⟩) ≠ 𝑍)))
3834, 36, 10, 37syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (⟨𝐶, 𝑦⟩ ∈ (𝐹 supp 𝑍) ↔ (⟨𝐶, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ (𝐹‘⟨𝐶, 𝑦⟩) ≠ 𝑍)))
3938ad2antrr 725 . . . . . . . . . 10 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (⟨𝐶, 𝑦⟩ ∈ (𝐹 supp 𝑍) ↔ (⟨𝐶, 𝑦⟩ ∈ (𝐴 × 𝐵) ∧ (𝐹‘⟨𝐶, 𝑦⟩) ≠ 𝑍)))
4026, 33, 39mpbir2and 712 . . . . . . . . 9 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → ⟨𝐶, 𝑦⟩ ∈ (𝐹 supp 𝑍))
41 simpr 488 . . . . . . . . . . 11 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → 𝑧 = ⟨𝐶, 𝑦⟩)
4241fveq2d 6654 . . . . . . . . . 10 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → ((2nd ↾ (V × V))‘𝑧) = ((2nd ↾ (V × V))‘⟨𝐶, 𝑦⟩))
43 xpss 5536 . . . . . . . . . . . 12 (𝐴 × 𝐵) ⊆ (V × V)
4426adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → ⟨𝐶, 𝑦⟩ ∈ (𝐴 × 𝐵))
4543, 44sseldi 3913 . . . . . . . . . . 11 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → ⟨𝐶, 𝑦⟩ ∈ (V × V))
4645fvresd 6670 . . . . . . . . . 10 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → ((2nd ↾ (V × V))‘⟨𝐶, 𝑦⟩) = (2nd ‘⟨𝐶, 𝑦⟩))
4724adantr 484 . . . . . . . . . . 11 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → 𝐶𝐴)
4825adantr 484 . . . . . . . . . . 11 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → 𝑦𝐵)
49 op2ndg 7691 . . . . . . . . . . 11 ((𝐶𝐴𝑦𝐵) → (2nd ‘⟨𝐶, 𝑦⟩) = 𝑦)
5047, 48, 49syl2anc 587 . . . . . . . . . 10 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → (2nd ‘⟨𝐶, 𝑦⟩) = 𝑦)
5142, 46, 503eqtrd 2837 . . . . . . . . 9 ((((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝐶, 𝑦⟩) → ((2nd ↾ (V × V))‘𝑧) = 𝑦)
5240, 51rspcedeq1vd 3577 . . . . . . . 8 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → ∃𝑧 ∈ (𝐹 supp 𝑍)((2nd ↾ (V × V))‘𝑧) = 𝑦)
53 fofn 6570 . . . . . . . . . . . . 13 (2nd :V–onto→V → 2nd Fn V)
54 fnresin 30399 . . . . . . . . . . . . 13 (2nd Fn V → (2nd ↾ (V × V)) Fn (V ∩ (V × V)))
5511, 53, 54mp2b 10 . . . . . . . . . . . 12 (2nd ↾ (V × V)) Fn (V ∩ (V × V))
56 ssv 3939 . . . . . . . . . . . . . 14 (V × V) ⊆ V
57 sseqin2 4142 . . . . . . . . . . . . . 14 ((V × V) ⊆ V ↔ (V ∩ (V × V)) = (V × V))
5856, 57mpbi 233 . . . . . . . . . . . . 13 (V ∩ (V × V)) = (V × V)
5958fneq2i 6424 . . . . . . . . . . . 12 ((2nd ↾ (V × V)) Fn (V ∩ (V × V)) ↔ (2nd ↾ (V × V)) Fn (V × V))
6055, 59mpbi 233 . . . . . . . . . . 11 (2nd ↾ (V × V)) Fn (V × V)
6160a1i 11 . . . . . . . . . 10 (𝜑 → (2nd ↾ (V × V)) Fn (V × V))
62 suppssdm 7833 . . . . . . . . . . . 12 (𝐹 supp 𝑍) ⊆ dom 𝐹
6334fndmd 6430 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = (𝐴 × 𝐵))
6462, 63sseqtrid 3967 . . . . . . . . . . 11 (𝜑 → (𝐹 supp 𝑍) ⊆ (𝐴 × 𝐵))
6564, 43sstrdi 3927 . . . . . . . . . 10 (𝜑 → (𝐹 supp 𝑍) ⊆ (V × V))
6661, 65fvelimabd 6718 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((2nd ↾ (V × V))‘𝑧) = 𝑦))
6766ad2antrr 725 . . . . . . . 8 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((2nd ↾ (V × V))‘𝑧) = 𝑦))
6852, 67mpbird 260 . . . . . . 7 (((𝜑𝑦𝐵) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)))
6968ex 416 . . . . . 6 ((𝜑𝑦𝐵) → (¬ (𝐺𝑦) = 𝑍𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍))))
7069con1d 147 . . . . 5 ((𝜑𝑦𝐵) → (¬ 𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)) → (𝐺𝑦) = 𝑍))
7170impr 458 . . . 4 ((𝜑 ∧ (𝑦𝐵 ∧ ¬ 𝑦 ∈ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)))) → (𝐺𝑦) = 𝑍)
7222, 71sylan2b 596 . . 3 ((𝜑𝑦 ∈ (𝐵 ∖ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)))) → (𝐺𝑦) = 𝑍)
7321, 72suppss 7850 . 2 (𝜑 → (𝐺 supp 𝑍) ⊆ ((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)))
74 suppssfifsupp 8839 . 2 (((𝐺 ∈ V ∧ Fun 𝐺𝑍𝑈) ∧ (((2nd ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin ∧ (𝐺 supp 𝑍) ⊆ ((2nd ↾ (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 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  ∃wrex 3107  Vcvv 3441   ∖ cdif 3878   ∩ cin 3880   ⊆ wss 3881  ⟨cop 4531   class class class wbr 5031   ↦ cmpt 5111   × cxp 5518  dom cdm 5520   ↾ cres 5522   “ cima 5523  Fun wfun 6321   Fn wfn 6322  –onto→wfo 6325  ‘cfv 6327  (class class class)co 7140  2nd c2nd 7677   supp csupp 7820  Fincfn 8499   finSupp cfsupp 8824 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7448 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-ord 6165  df-on 6166  df-lim 6167  df-suc 6168  df-iota 6286  df-fun 6329  df-fn 6330  df-f 6331  df-f1 6332  df-fo 6333  df-f1o 6334  df-fv 6335  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7568  df-2nd 7679  df-supp 7821  df-1o 8092  df-er 8279  df-en 8500  df-dom 8501  df-fin 8503  df-fsupp 8825 This theorem is referenced by:  fedgmullem2  31150
 Copyright terms: Public domain W3C validator