suppeqfsuppbi

Description: If two functions have the same support, one function is finitely supported iff the other one is finitely supported. (Contributed by AV, 30-Jun-2019)

		Ref	Expression
	Assertion	suppeqfsuppbi	$⊢ ((F \in U \land Fun F) \land (G \in V \land Fun G)) \to (F supp Z = G supp Z \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} (G)))$

Proof

Step	Hyp	Ref	Expression
1		simprlr	$⊢ (Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \to Fun F$
2		simprll	$⊢ (Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \to F \in U$
3		simpl	$⊢ (Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \to Z \in V$
4		funisfsupp	$⊢ (Fun F \land F \in U \land Z \in V) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
5	1 2 3 4	syl3anc	$⊢ (Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
6	5	adantr	$⊢ ((Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \land F supp Z = G supp Z) \to ({finSupp}_{Z} (F) \leftrightarrow F supp Z \in Fin)$
7		simpr	$⊢ (G \in V \land Fun G) \to Fun G$
8	7	adantr	$⊢ ((G \in V \land Fun G) \land Z \in V) \to Fun G$
9		simpl	$⊢ (G \in V \land Fun G) \to G \in V$
10	9	adantr	$⊢ ((G \in V \land Fun G) \land Z \in V) \to G \in V$
11		simpr	$⊢ ((G \in V \land Fun G) \land Z \in V) \to Z \in V$
12		funisfsupp	$⊢ (Fun G \land G \in V \land Z \in V) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
13	8 10 11 12	syl3anc	$⊢ ((G \in V \land Fun G) \land Z \in V) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
14	13	ex	$⊢ (G \in V \land Fun G) \to (Z \in V \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin))$
15	14	adantl	$⊢ ((F \in U \land Fun F) \land (G \in V \land Fun G)) \to (Z \in V \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin))$
16	15	impcom	$⊢ (Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \to ({finSupp}_{Z} (G) \leftrightarrow G supp Z \in Fin)$
17		eleq1	$⊢ F supp Z = G supp Z \to (F supp Z \in Fin \leftrightarrow G supp Z \in Fin)$
18	17	bicomd	$⊢ F supp Z = G supp Z \to (G supp Z \in Fin \leftrightarrow F supp Z \in Fin)$
19	16 18	sylan9bb	$⊢ ((Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \land F supp Z = G supp Z) \to ({finSupp}_{Z} (G) \leftrightarrow F supp Z \in Fin)$
20	6 19	bitr4d	$⊢ ((Z \in V \land ((F \in U \land Fun F) \land (G \in V \land Fun G))) \land F supp Z = G supp Z) \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} (G))$
21	20	exp31	$⊢ Z \in V \to (((F \in U \land Fun F) \land (G \in V \land Fun G)) \to (F supp Z = G supp Z \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} (G))))$
22		relfsupp	$⊢ Rel finSupp$
23	22	brrelex2i	$⊢ {finSupp}_{Z} (F) \to Z \in V$
24	22	brrelex2i	$⊢ {finSupp}_{Z} (G) \to Z \in V$
25	23 24	pm5.21ni	$⊢ \neg Z \in V \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} (G))$
26	25	2a1d	$⊢ \neg Z \in V \to (((F \in U \land Fun F) \land (G \in V \land Fun G)) \to (F supp Z = G supp Z \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} (G))))$
27	21 26	pm2.61i	$⊢ ((F \in U \land Fun F) \land (G \in V \land Fun G)) \to (F supp Z = G supp Z \to ({finSupp}_{Z} (F) \leftrightarrow {finSupp}_{Z} (G)))$

Metamath Proof Explorer

Theorem suppeqfsuppbi

Proof