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	rspcedeqvd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ ( 𝐺 ‘ 𝑦 ) = 𝑍 ) → ∃ 𝑧 ∈ ( 𝐹 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 𝑍 )