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	biimpi	$⊢ (F \cup G) supp Z \in Fin \to (G \cup F) supp Z \in Fin$
24	23	adantl	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to (G \cup F) supp Z \in Fin$
25	24	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$
26	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$
27	25 26	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$
28	10	simprd	$⊢ Fun (F \cup G) \to Fun G$
29	28	adantr	$⊢ (Fun (F \cup G) \land (F \cup G) supp Z \in Fin) \to Fun G$
30	29	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$
31		funisfsupp	$⊢ (Fun G \land G \in V \land Z \in V) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
32	30 7 16 31	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)$
33	27 32	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)$
34	19 33	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))$
35	34	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)))$
36	35	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))))$
37		fsuppimp	$⊢ {finSupp}_{Z} ((F \cup G)) \to (Fun (F \cup G) \land (F \cup G) supp Z \in Fin)$
38	36 37	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))))$
39	4 38	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))))$
40	3 39	mpcom	$⊢ {finSupp}_{Z} ((F \cup G)) \to (φ \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$
41	40	com12	$⊢ φ \to ({finSupp}_{Z} ((F \cup G)) \to ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$
42		simpl	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to {finSupp}_{Z} (F)$
43		simpr	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to {finSupp}_{Z} (G)$
44	42 43	fsuppun	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to (F \cup G) supp Z \in Fin$
45	44	adantl	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to (F \cup G) supp Z \in Fin$
46	1	adantr	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to Fun (F \cup G)$
47	2	brrelex1i	$⊢ {finSupp}_{Z} (F) \to F \in V$
48	2	brrelex1i	$⊢ {finSupp}_{Z} (G) \to G \in V$
49		unexg	$⊢ (F \in V \land G \in V) \to F \cup G \in V$
50	47 48 49	syl2an	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to F \cup G \in V$
51	50	adantl	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to F \cup G \in V$
52	2	brrelex2i	$⊢ {finSupp}_{Z} (F) \to Z \in V$
53	52	adantr	$⊢ ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to Z \in V$
54	53	adantl	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to Z \in V$
55		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)$
56	46 51 54 55	syl3anc	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to ({finSupp}_{Z} ((F \cup G)) \leftrightarrow (F \cup G) supp Z \in Fin)$
57	45 56	mpbird	$⊢ (φ \land ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G))) \to {finSupp}_{Z} ((F \cup G))$
58	57	ex	$⊢ φ \to (({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)) \to {finSupp}_{Z} ((F \cup G)))$
59	41 58	impbid	$⊢ φ \to ({finSupp}_{Z} ((F \cup G)) \leftrightarrow ({finSupp}_{Z} (F) \land {finSupp}_{Z} (G)))$

Metamath Proof Explorer

Theorem fsuppunbi

Proof