fsuppcurry1

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

	Ref	Expression
Hypotheses	fsuppcurry1.g	$⊢ G = (x \in B ⟼ C F x)$
	fsuppcurry1.z	$⊢ φ \to Z \in U$
	fsuppcurry1.a	$⊢ φ \to A \in V$
	fsuppcurry1.b	$⊢ φ \to B \in W$
	fsuppcurry1.f	$⊢ φ \to F Fn (A \times B)$
	fsuppcurry1.c	$⊢ φ \to C \in A$
	fsuppcurry1.1	$⊢ φ \to {finSupp}_{Z} (F)$
Assertion	fsuppcurry1	$⊢ φ \to {finSupp}_{Z} (G)$

Proof

Step	Hyp	Ref	Expression
1		fsuppcurry1.g	$⊢ G = (x \in B ⟼ C F x)$
2		fsuppcurry1.z	$⊢ φ \to Z \in U$
3		fsuppcurry1.a	$⊢ φ \to A \in V$
4		fsuppcurry1.b	$⊢ φ \to B \in W$
5		fsuppcurry1.f	$⊢ φ \to F Fn (A \times B)$
6		fsuppcurry1.c	$⊢ φ \to C \in A$
7		fsuppcurry1.1	$⊢ φ \to {finSupp}_{Z} (F)$
8		oveq2	$⊢ x = y \to C F x = C F y$
9	8	cbvmptv	$⊢ (x \in B ⟼ C F x) = (y \in B ⟼ C F y)$
10	1 9	eqtri	$⊢ G = (y \in B ⟼ C F y)$
11	4	mptexd	$⊢ φ \to (y \in B ⟼ C F y) \in V$
12	10 11	eqeltrid	$⊢ φ \to G \in V$
13	1	funmpt2	$⊢ Fun G$
14	13	a1i	$⊢ φ \to Fun G$
15		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
16		fofun	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to Fun 2^{nd}$
17	15 16	ax-mp	$⊢ Fun 2^{nd}$
18		funres	$⊢ Fun 2^{nd} \to Fun ({2^{nd} ↾}_{(V \times V)})$
19	17 18	mp1i	$⊢ φ \to Fun ({2^{nd} ↾}_{(V \times V)})$
20	7	fsuppimpd	$⊢ φ \to F supp Z \in Fin$
21		imafi	$⊢ (Fun ({2^{nd} ↾}_{(V \times V)}) \land F supp Z \in Fin) \to ({2^{nd} ↾}_{(V \times V)}) [F supp Z] \in Fin$
22	19 20 21	syl2anc	$⊢ φ \to ({2^{nd} ↾}_{(V \times V)}) [F supp Z] \in Fin$
23		ovexd	$⊢ (φ \land y \in B) \to C F y \in V$
24	23 10	fmptd	$⊢ φ \to G : B ⟶ V$
25		eldif	$⊢ y \in (B ∖ ({2^{nd} ↾}_{(V \times V)}) [F supp Z]) \leftrightarrow (y \in B \land \neg y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z])$
26	6	ad2antrr	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to C \in A$
27		simplr	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to y \in B$
28	26 27	opelxpd	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to ⟨C, y⟩ \in (A \times B)$
29		df-ov	$⊢ C F y = F (⟨C, y⟩)$
30		ovexd	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to C F y \in V$
31	1 8 27 30	fvmptd3	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to G (y) = C F y$
32		simpr	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to \neg G (y) = Z$
33	32	neqned	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to G (y) \neq Z$
34	31 33	eqnetrrd	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to C F y \neq Z$
35	29 34	eqnetrrid	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to F (⟨C, y⟩) \neq Z$
36	3 4	xpexd	$⊢ φ \to A \times B \in V$
37		elsuppfn	$⊢ (F Fn (A \times B) \land A \times B \in V \land Z \in U) \to (⟨C, y⟩ \in {supp}_{Z} (F) \leftrightarrow (⟨C, y⟩ \in (A \times B) \land F (⟨C, y⟩) \neq Z))$
38	5 36 2 37	syl3anc	$⊢ φ \to (⟨C, y⟩ \in {supp}_{Z} (F) \leftrightarrow (⟨C, y⟩ \in (A \times B) \land F (⟨C, y⟩) \neq Z))$
39	38	ad2antrr	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to (⟨C, y⟩ \in {supp}_{Z} (F) \leftrightarrow (⟨C, y⟩ \in (A \times B) \land F (⟨C, y⟩) \neq Z))$
40	28 35 39	mpbir2and	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to ⟨C, y⟩ \in {supp}_{Z} (F)$
41		simpr	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to z = ⟨C, y⟩$
42	41	fveq2d	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to ({2^{nd} ↾}_{(V \times V)}) (z) = ({2^{nd} ↾}_{(V \times V)}) (⟨C, y⟩)$
43		xpss	$⊢ A \times B \subseteq V \times V$
44	28	adantr	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to ⟨C, y⟩ \in (A \times B)$
45	43 44	sselid	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to ⟨C, y⟩ \in (V \times V)$
46	45	fvresd	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to ({2^{nd} ↾}_{(V \times V)}) (⟨C, y⟩) = 2^{nd} (⟨C, y⟩)$
47	26	adantr	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to C \in A$
48	27	adantr	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to y \in B$
49		op2ndg	$⊢ (C \in A \land y \in B) \to 2^{nd} (⟨C, y⟩) = y$
50	47 48 49	syl2anc	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to 2^{nd} (⟨C, y⟩) = y$
51	42 46 50	3eqtrd	$⊢ (((φ \land y \in B) \land \neg G (y) = Z) \land z = ⟨C, y⟩) \to ({2^{nd} ↾}_{(V \times V)}) (z) = y$
52	40 51	rspcedeq1vd	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to \exists z \in {supp}_{Z} (F) ({2^{nd} ↾}_{(V \times V)}) (z) = y$
53		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
54		fnresin	$⊢ 2^{nd} Fn V \to ({2^{nd} ↾}_{(V \times V)}) Fn (V \cap (V \times V))$
55	15 53 54	mp2b	$⊢ ({2^{nd} ↾}_{(V \times V)}) Fn (V \cap (V \times V))$
56		ssv	$⊢ V \times V \subseteq V$
57		sseqin2	$⊢ V \times V \subseteq V \leftrightarrow V \cap (V \times V) = V \times V$
58	56 57	mpbi	$⊢ V \cap (V \times V) = V \times V$
59	58	fneq2i	$⊢ ({2^{nd} ↾}_{(V \times V)}) Fn (V \cap (V \times V)) \leftrightarrow ({2^{nd} ↾}_{(V \times V)}) Fn (V \times V)$
60	55 59	mpbi	$⊢ ({2^{nd} ↾}_{(V \times V)}) Fn (V \times V)$
61	60	a1i	$⊢ φ \to ({2^{nd} ↾}_{(V \times V)}) Fn (V \times V)$
62		suppssdm	$⊢ F supp Z \subseteq dom F$
63	5	fndmd	$⊢ φ \to dom F = A \times B$
64	62 63	sseqtrid	$⊢ φ \to F supp Z \subseteq A \times B$
65	64 43	sstrdi	$⊢ φ \to F supp Z \subseteq V \times V$
66	61 65	fvelimabd	$⊢ φ \to (y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z] \leftrightarrow \exists z \in {supp}_{Z} (F) ({2^{nd} ↾}_{(V \times V)}) (z) = y)$
67	66	ad2antrr	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to (y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z] \leftrightarrow \exists z \in {supp}_{Z} (F) ({2^{nd} ↾}_{(V \times V)}) (z) = y)$
68	52 67	mpbird	$⊢ ((φ \land y \in B) \land \neg G (y) = Z) \to y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z]$
69	68	ex	$⊢ (φ \land y \in B) \to (\neg G (y) = Z \to y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z])$
70	69	con1d	$⊢ (φ \land y \in B) \to (\neg y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z] \to G (y) = Z)$
71	70	impr	$⊢ (φ \land (y \in B \land \neg y \in ({2^{nd} ↾}_{(V \times V)}) [F supp Z])) \to G (y) = Z$
72	25 71	sylan2b	$⊢ (φ \land y \in (B ∖ ({2^{nd} ↾}_{(V \times V)}) [F supp Z])) \to G (y) = Z$
73	24 72	suppss	$⊢ φ \to G supp Z \subseteq ({2^{nd} ↾}_{(V \times V)}) [F supp Z]$
74		suppssfifsupp	$⊢ ((G \in V \land Fun G \land Z \in U) \land (({2^{nd} ↾}_{(V \times V)}) [F supp Z] \in Fin \land G supp Z \subseteq ({2^{nd} ↾}_{(V \times V)}) [F supp Z])) \to {finSupp}_{Z} (G)$
75	12 14 2 22 73 74	syl32anc	$⊢ φ \to {finSupp}_{Z} (G)$

Metamath Proof Explorer

Theorem fsuppcurry1

Proof