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

Theorem fsuppcurry2 30498
 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 7143 . . . . 5 (𝑥 = 𝑦 → (𝑥𝐹𝐶) = (𝑦𝐹𝐶))
32cbvmptv 5134 . . . 4 (𝑥𝐴 ↦ (𝑥𝐹𝐶)) = (𝑦𝐴 ↦ (𝑦𝐹𝐶))
41, 3eqtri 2821 . . 3 𝐺 = (𝑦𝐴 ↦ (𝑦𝐹𝐶))
5 fsuppcurry2.a . . . 4 (𝜑𝐴𝑉)
65mptexd 6965 . . 3 (𝜑 → (𝑦𝐴 ↦ (𝑦𝐹𝐶)) ∈ V)
74, 6eqeltrid 2894 . 2 (𝜑𝐺 ∈ V)
81funmpt2 6364 . . 3 Fun 𝐺
98a1i 11 . 2 (𝜑 → Fun 𝐺)
10 fsuppcurry2.z . 2 (𝜑𝑍𝑈)
11 fo1st 7694 . . . . 5 1st :V–onto→V
12 fofun 6567 . . . . 5 (1st :V–onto→V → Fun 1st )
1311, 12ax-mp 5 . . . 4 Fun 1st
14 funres 6367 . . . 4 (Fun 1st → Fun (1st ↾ (V × V)))
1513, 14mp1i 13 . . 3 (𝜑 → Fun (1st ↾ (V × V)))
16 fsuppcurry2.1 . . . 4 (𝜑𝐹 finSupp 𝑍)
1716fsuppimpd 8827 . . 3 (𝜑 → (𝐹 supp 𝑍) ∈ Fin)
18 imafi 8804 . . 3 ((Fun (1st ↾ (V × V)) ∧ (𝐹 supp 𝑍) ∈ Fin) → ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin)
1915, 17, 18syl2anc 587 . 2 (𝜑 → ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ∈ Fin)
20 ovexd 7171 . . . 4 ((𝜑𝑦𝐴) → (𝑦𝐹𝐶) ∈ V)
2120, 4fmptd 6856 . . 3 (𝜑𝐺:𝐴⟶V)
22 eldif 3891 . . . 4 (𝑦 ∈ (𝐴 ∖ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍))) ↔ (𝑦𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍))))
23 simplr 768 . . . . . . . . . . 11 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝑦𝐴)
24 fsuppcurry2.c . . . . . . . . . . . 12 (𝜑𝐶𝐵)
2524ad2antrr 725 . . . . . . . . . . 11 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝐶𝐵)
2623, 25opelxpd 5558 . . . . . . . . . 10 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵))
27 df-ov 7139 . . . . . . . . . . 11 (𝑦𝐹𝐶) = (𝐹‘⟨𝑦, 𝐶⟩)
28 ovexd 7171 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦𝐹𝐶) ∈ V)
291, 2, 23, 28fvmptd3 6769 . . . . . . . . . . . 12 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐺𝑦) = (𝑦𝐹𝐶))
30 simpr 488 . . . . . . . . . . . . 13 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ¬ (𝐺𝑦) = 𝑍)
3130neqned 2994 . . . . . . . . . . . 12 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐺𝑦) ≠ 𝑍)
3229, 31eqnetrrd 3055 . . . . . . . . . . 11 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦𝐹𝐶) ≠ 𝑍)
3327, 32eqnetrrid 3062 . . . . . . . . . 10 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝐹‘⟨𝑦, 𝐶⟩) ≠ 𝑍)
34 fsuppcurry2.f . . . . . . . . . . . 12 (𝜑𝐹 Fn (𝐴 × 𝐵))
35 fsuppcurry2.b . . . . . . . . . . . . 13 (𝜑𝐵𝑊)
365, 35xpexd 7457 . . . . . . . . . . . 12 (𝜑 → (𝐴 × 𝐵) ∈ V)
37 elsuppfn 7824 . . . . . . . . . . . 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 6650 . . . . . . . . . 10 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ((1st ↾ (V × V))‘𝑧) = ((1st ↾ (V × V))‘⟨𝑦, 𝐶⟩))
43 xpss 5536 . . . . . . . . . . . 12 (𝐴 × 𝐵) ⊆ (V × V)
4426adantr 484 . . . . . . . . . . . 12 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ⟨𝑦, 𝐶⟩ ∈ (𝐴 × 𝐵))
4543, 44sseldi 3913 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ⟨𝑦, 𝐶⟩ ∈ (V × V))
4645fvresd 6666 . . . . . . . . . 10 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ((1st ↾ (V × V))‘⟨𝑦, 𝐶⟩) = (1st ‘⟨𝑦, 𝐶⟩))
4723adantr 484 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → 𝑦𝐴)
4825adantr 484 . . . . . . . . . . 11 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → 𝐶𝐵)
49 op1stg 7686 . . . . . . . . . . 11 ((𝑦𝐴𝐶𝐵) → (1st ‘⟨𝑦, 𝐶⟩) = 𝑦)
5047, 48, 49syl2anc 587 . . . . . . . . . 10 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → (1st ‘⟨𝑦, 𝐶⟩) = 𝑦)
5142, 46, 503eqtrd 2837 . . . . . . . . 9 ((((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) ∧ 𝑧 = ⟨𝑦, 𝐶⟩) → ((1st ↾ (V × V))‘𝑧) = 𝑦)
5240, 51rspcedeq1vd 3577 . . . . . . . 8 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V × V))‘𝑧) = 𝑦)
53 fofn 6568 . . . . . . . . . . . . 13 (1st :V–onto→V → 1st Fn V)
54 fnresin 30395 . . . . . . . . . . . . 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 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 6422 . . . . . . . . . . . 12 ((1st ↾ (V × V)) Fn (V ∩ (V × V)) ↔ (1st ↾ (V × V)) Fn (V × V))
6055, 59mpbi 233 . . . . . . . . . . 11 (1st ↾ (V × V)) Fn (V × V)
6160a1i 11 . . . . . . . . . 10 (𝜑 → (1st ↾ (V × V)) Fn (V × V))
62 suppssdm 7829 . . . . . . . . . . . 12 (𝐹 supp 𝑍) ⊆ dom 𝐹
6334fndmd 6428 . . . . . . . . . . . 12 (𝜑 → dom 𝐹 = (𝐴 × 𝐵))
6462, 63sseqtrid 3967 . . . . . . . . . . 11 (𝜑 → (𝐹 supp 𝑍) ⊆ (𝐴 × 𝐵))
6564, 43sstrdi 3927 . . . . . . . . . 10 (𝜑 → (𝐹 supp 𝑍) ⊆ (V × V))
6661, 65fvelimabd 6714 . . . . . . . . 9 (𝜑 → (𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V × V))‘𝑧) = 𝑦))
6766ad2antrr 725 . . . . . . . 8 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → (𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) ↔ ∃𝑧 ∈ (𝐹 supp 𝑍)((1st ↾ (V × V))‘𝑧) = 𝑦))
6852, 67mpbird 260 . . . . . . 7 (((𝜑𝑦𝐴) ∧ ¬ (𝐺𝑦) = 𝑍) → 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))
6968ex 416 . . . . . 6 ((𝜑𝑦𝐴) → (¬ (𝐺𝑦) = 𝑍𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍))))
7069con1d 147 . . . . 5 ((𝜑𝑦𝐴) → (¬ 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)) → (𝐺𝑦) = 𝑍))
7170impr 458 . . . 4 ((𝜑 ∧ (𝑦𝐴 ∧ ¬ 𝑦 ∈ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))) → (𝐺𝑦) = 𝑍)
7222, 71sylan2b 596 . . 3 ((𝜑𝑦 ∈ (𝐴 ∖ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))) → (𝐺𝑦) = 𝑍)
7321, 72suppss 7846 . 2 (𝜑 → (𝐺 supp 𝑍) ⊆ ((1st ↾ (V × V)) “ (𝐹 supp 𝑍)))
74 suppssfifsupp 8835 . 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 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 6319   Fn wfn 6320  –onto→wfo 6323  ‘cfv 6325  (class class class)co 7136  1st c1st 7672   supp csupp 7816  Fincfn 8495   finSupp cfsupp 8820 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 7444 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 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-supp 7817  df-1o 8088  df-er 8275  df-en 8496  df-dom 8497  df-fin 8499  df-fsupp 8821 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator