fsuppunbi

Description: If the union of two classes/functions is a function, this union is finitely supported iff the two functions are finitely supported. (Contributed by AV, 18-Jun-2019)

		Ref	Expression
	Hypothesis	fsuppunbi.u	$⊢ φ \to Fun (F \cup G)$
	Assertion	fsuppunbi	$⊢ φ \to ({finSupp}_{Z} ((F \cup G)) \leftrightarrow ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$

Proof

Step	Hyp	Ref	Expression
1		fsuppunbi.u	$⊢ φ \to Fun (F \cup G)$
2		relfsupp	$⊢ Rel finSupp$
3	2	brrelex12i	$⊢ {finSupp}_{Z} ((F \cup G)) \to (F \cup G \in V \land Z \in V)$
4		unexb	$⊢ (F \in V \land G \in V) \leftrightarrow F \cup G \in V$
5		simpr	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to (F \cup G) supp Z \in Fin$
6	5	adantr	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to (F \cup G) supp Z \in Fin$
7		simprlr	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to G \in V$
8	7	suppun	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to F supp Z \subseteq (F \cup G) supp Z$
9	6 8	ssfid	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to F supp Z \in Fin$
10		fununfun	$⊢ Fun (F \cup G) \to (Fun F \land Fun G)$
11	10	simpld	$⊢ Fun (F \cup G) \to Fun F$
12	11	adantr	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to Fun F$
13	12	adantr	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to Fun F$
14		simprll	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to F \in V$
15		simpr	$⊢ ((F \in V \land G \in V) \land Z \in V) \to Z \in V$
16	15	adantl	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to Z \in V$
17		funisfsupp	$⊢ (Fun F \land F \in V \land Z \in V) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
18	13 14 16 17	syl3anc	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
19	9 18	mpbird	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to {finSupp}_{Z} (F)$
20		uncom	$⊢ F \cup G = G \cup F$
21	20	oveq1i	$⊢ (F \cup G) supp Z = (G \cup F) supp Z$
22	21	eleq1i	$⊢ (F \cup G) supp Z \in Fin \leftrightarrow (G \cup F) supp Z \in Fin$
23	22	bilani	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to (G \cup F) supp Z \in Fin$
24	23	adantr	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to (G \cup F) supp Z \in Fin$
25	14	suppun	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to G supp Z \subseteq (G \cup F) supp Z$
26	24 25	ssfid	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to G supp Z \in Fin$
27	10	simprd	$⊢ Fun (F \cup G) \to Fun G$
28	27	adantr	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to Fun G$
29	28	adantr	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to Fun G$
30		funisfsupp	$⊢ (Fun G \land G \in V \land Z \in V) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
31	29 7 16 30	syl3anc	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
32	26 31	mpbird	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to {finSupp}_{Z} (G)$
33	19 32	jca	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))$
34	33	a1d	$⊢ ((Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \land ((F \in V \land G \in V) \land Z \in V)) \to (φ \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$
35	34	ex	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to (((F \in V \land G \in V) \land Z \in V) \to (φ \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))))$
36		fsuppimp	$⊢ {finSupp}_{Z} ((F \cup G)) \to (Fun (F \cup G) \land (F \cup G) supp Z \in Fin)$
37	35 36	syl11	$⊢ ((F \in V \land G \in V) \land Z \in V) \to ({finSupp}_{Z} ((F \cup G)) \to (φ \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))))$
38	4 37	sylanbr	$⊢ (F \cup G \in V \land Z \in V) \to ({finSupp}_{Z} ((F \cup G)) \to (φ \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))))$
39	3 38	mpcom	$⊢ {finSupp}_{Z} ((F \cup G)) \to (φ \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$
40	39	com12	$⊢ φ \to ({finSupp}_{Z} ((F \cup G)) \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$
41		simpl	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to {finSupp}_{Z} (F)$
42		simpr	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to {finSupp}_{Z} (G)$
43	41 42	fsuppun	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to (F \cup G) supp Z \in Fin$
44	43	adantl	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to (F \cup G) supp Z \in Fin$
45	1	adantr	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to Fun (F \cup G)$
46	2	brrelex1i	$⊢ {finSupp}_{Z} (F) \to F \in V$
47	2	brrelex1i	$⊢ {finSupp}_{Z} (G) \to G \in V$
48		unexg	$⊢ (F \in V \land G \in V) \to F \cup G \in V$
49	46 47 48	syl2an	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to F \cup G \in V$
50	49	adantl	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to F \cup G \in V$
51	2	brrelex2i	$⊢ {finSupp}_{Z} (F) \to Z \in V$
52	51	adantr	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to Z \in V$
53	52	adantl	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to Z \in V$
54		funisfsupp	$⊢ (Fun (F \cup G) \land F \cup G \in V \land Z \in V) \to ({finSupp}_{Z} ((F \cup G)) \leftrightarrow (F \cup G) supp Z \in Fin)$
55	45 50 53 54	syl3anc	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to ({finSupp}_{Z} ((F \cup G)) \leftrightarrow (F \cup G) supp Z \in Fin)$
56	44 55	mpbird	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to {finSupp}_{Z} ((F \cup G))$
57	56	ex	$⊢ φ \to (({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to {finSupp}_{Z} ((F \cup G)))$
58	40 57	impbid	$⊢ φ \to ({finSupp}_{Z} ((F \cup G)) \leftrightarrow ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$

Metamath Proof Explorer

Theorem fsuppunbi

Proof