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	$⊢ G = (x \in A ⟼ x F C)$
	fsuppcurry2.z	$⊢ φ \to Z \in U$
	fsuppcurry2.a	$⊢ φ \to A \in V$
	fsuppcurry2.b	$⊢ φ \to B \in W$
	fsuppcurry2.f	$⊢ φ \to F Fn (A \times B)$
	fsuppcurry2.c	$⊢ φ \to C \in B$
	fsuppcurry2.1	$⊢ φ \to {finSupp}_{Z} (F)$
Assertion	fsuppcurry2	$⊢ φ \to {finSupp}_{Z} (G)$

Proof

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

Proof