Metamath Proof Explorer

Theorem fsuppcurry2

Description: Finite support of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 7-Jul-2023)

Ref Expression
Hypotheses fsuppcurry2.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) )
fsuppcurry2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
fsuppcurry2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
fsuppcurry2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
fsuppcurry2.f ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
fsuppcurry2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
fsuppcurry2.1 ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
Assertion fsuppcurry2 ( 𝜑 → 𝐺 finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 fsuppcurry2.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) )
2 fsuppcurry2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑈 )
3 fsuppcurry2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 fsuppcurry2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5 fsuppcurry2.f ⊢ ( 𝜑 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
6 fsuppcurry2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
7 fsuppcurry2.1 ⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
8 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 𝐹 𝐶 ) = ( 𝑦 𝐹 𝐶 ) )
9 8 cbvmptv ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝑥 𝐹 𝐶 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝑦 𝐹 𝐶 ) )
10 1 9 eqtri ⊢ 𝐺 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑦 𝐹 𝐶 ) )
11 3 mptexd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( 𝑦 𝐹 𝐶 ) ) ∈ V )
12 10 11 eqeltrid ⊢ ( 𝜑 → 𝐺 ∈ V )
13 1 funmpt2 ⊢ Fun 𝐺
14 13 a1i ⊢ ( 𝜑 → Fun 𝐺 )
15 fo1st ⊢ 1st : V –onto→ V
16 fofun ⊢ ( 1st : V –onto→ V → Fun 1st )
17 15 16 ax-mp ⊢ Fun 1st
18 funres ⊢ ( Fun 1st → Fun ( 1st ↾ ( V × V ) ) )
19 17 18 mp1i ⊢ ( 𝜑 → Fun ( 1st ↾ ( V × V ) ) )
20 7 fsuppimpd ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ∈ Fin )
21 imafi ⊢ ( ( Fun ( 1st ↾ ( V × V ) ) ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) → ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ∈ Fin )
22 19 20 21 syl2anc ⊢ ( 𝜑 → ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ∈ Fin )
23 ovexd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝐹 𝐶 ) ∈ V )
24 23 10 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ V )
25 eldif ⊢ ( 𝑦 ∈ ( 𝐴 ∖ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ) ↔ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ) )
26 simplr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → 𝑦 ∈ 𝐴 )
27 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → 𝐶 ∈ 𝐵 )
28 26 27 opelxpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐵 ) )
29 df-ov ⊢ ( 𝑦 𝐹 𝐶 ) = ( 𝐹 ‘ ⟨ 𝑦 , 𝐶 ⟩ )
30 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( 𝑦 𝐹 𝐶 ) ∈ V )
31 1 8 26 30 fvmptd3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝑦 𝐹 𝐶 ) )
32 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 )
33 32 neqned ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( 𝐺 ‘ 𝑦 ) ≠ 𝑍 )
34 31 33 eqnetrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( 𝑦 𝐹 𝐶 ) ≠ 𝑍 )
35 29 34 eqnetrrid ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( 𝐹 ‘ ⟨ 𝑦 , 𝐶 ⟩ ) ≠ 𝑍 )
36 3 4 xpexd ⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
37 elsuppfn ⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝐴 × 𝐵 ) ∈ V ∧ 𝑍 ∈ 𝑈 ) → ( ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐹 supp 𝑍 ) ↔ ( ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑦 , 𝐶 ⟩ ) ≠ 𝑍 ) ) )
38 5 36 2 37 syl3anc ⊢ ( 𝜑 → ( ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐹 supp 𝑍 ) ↔ ( ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑦 , 𝐶 ⟩ ) ≠ 𝑍 ) ) )
39 38 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐹 supp 𝑍 ) ↔ ( ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐵 ) ∧ ( 𝐹 ‘ ⟨ 𝑦 , 𝐶 ⟩ ) ≠ 𝑍 ) ) )
40 28 35 39 mpbir2and ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐹 supp 𝑍 ) )
41 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ )
42 41 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → ( ( 1st ↾ ( V × V ) ) ‘ 𝑧 ) = ( ( 1st ↾ ( V × V ) ) ‘ ⟨ 𝑦 , 𝐶 ⟩ ) )
43 xpss ⊢ ( 𝐴 × 𝐵 ) ⊆ ( V × V )
44 28 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → ⟨ 𝑦 , 𝐶 ⟩ ∈ ( 𝐴 × 𝐵 ) )
45 43 44 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → ⟨ 𝑦 , 𝐶 ⟩ ∈ ( V × V ) )
46 45 fvresd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → ( ( 1st ↾ ( V × V ) ) ‘ ⟨ 𝑦 , 𝐶 ⟩ ) = ( 1st ‘ ⟨ 𝑦 , 𝐶 ⟩ ) )
47 26 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → 𝑦 ∈ 𝐴 )
48 27 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → 𝐶 ∈ 𝐵 )
49 op1stg ⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) → ( 1st ‘ ⟨ 𝑦 , 𝐶 ⟩ ) = 𝑦 )
50 47 48 49 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → ( 1st ‘ ⟨ 𝑦 , 𝐶 ⟩ ) = 𝑦 )
51 42 46 50 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) ∧ 𝑧 = ⟨ 𝑦 , 𝐶 ⟩ ) → ( ( 1st ↾ ( V × V ) ) ‘ 𝑧 ) = 𝑦 )
52 40 51 rspcedeq1vd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ∃ 𝑧 ∈ ( 𝐹 supp 𝑍 ) ( ( 1st ↾ ( V × V ) ) ‘ 𝑧 ) = 𝑦 )
53 fofn ⊢ ( 1st : V –onto→ V → 1st Fn V )
54 fnresin ⊢ ( 1st Fn V → ( 1st ↾ ( V × V ) ) Fn ( V ∩ ( V × V ) ) )
55 15 53 54 mp2b ⊢ ( 1st ↾ ( V × V ) ) Fn ( V ∩ ( V × V ) )
56 ssv ⊢ ( V × V ) ⊆ V
57 sseqin2 ⊢ ( ( V × V ) ⊆ V ↔ ( V ∩ ( V × V ) ) = ( V × V ) )
58 56 57 mpbi ⊢ ( V ∩ ( V × V ) ) = ( V × V )
59 58 fneq2i ⊢ ( ( 1st ↾ ( V × V ) ) Fn ( V ∩ ( V × V ) ) ↔ ( 1st ↾ ( V × V ) ) Fn ( V × V ) )
60 55 59 mpbi ⊢ ( 1st ↾ ( V × V ) ) Fn ( V × V )
61 60 a1i ⊢ ( 𝜑 → ( 1st ↾ ( V × V ) ) Fn ( V × V ) )
62 suppssdm ⊢ ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹
63 5 fndmd ⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 × 𝐵 ) )
64 62 63 sseqtrid ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( 𝐴 × 𝐵 ) )
65 64 43 sstrdi ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( V × V ) )
66 61 65 fvelimabd ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ↔ ∃ 𝑧 ∈ ( 𝐹 supp 𝑍 ) ( ( 1st ↾ ( V × V ) ) ‘ 𝑧 ) = 𝑦 ) )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ( 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ↔ ∃ 𝑧 ∈ ( 𝐹 supp 𝑍 ) ( ( 1st ↾ ( V × V ) ) ‘ 𝑧 ) = 𝑦 ) )
68 52 67 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) )
69 68 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 → 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ) )
70 69 con1d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) → ( 𝐺 ‘ 𝑦 ) = 𝑍 ) )
71 70 impr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ) ) → ( 𝐺 ‘ 𝑦 ) = 𝑍 )
72 25 71 sylan2b ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝐴 ∖ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ) ) → ( 𝐺 ‘ 𝑦 ) = 𝑍 )
73 24 72 suppss ⊢ ( 𝜑 → ( 𝐺 supp 𝑍 ) ⊆ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) )
74 suppssfifsupp ⊢ ( ( ( 𝐺 ∈ V ∧ Fun 𝐺 ∧ 𝑍 ∈ 𝑈 ) ∧ ( ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ∈ Fin ∧ ( 𝐺 supp 𝑍 ) ⊆ ( ( 1st ↾ ( V × V ) ) “ ( 𝐹 supp 𝑍 ) ) ) ) → 𝐺 finSupp 𝑍 )
75 12 14 2 22 73 74 syl32anc ⊢ ( 𝜑 → 𝐺 finSupp 𝑍 )