funsnfsupp

Description: Finite support for a function extended by a singleton. (Contributed by Stefan O'Rear, 27-Feb-2015) (Revised by AV, 19-Jul-2019)

		Ref	Expression
	Assertion	funsnfsupp	$⊢ ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow {finSupp}_{Z} (F))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to (X \in V \land Y \in W)$
2	1	anim2i	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to (Z \in V \land (X \in V \land Y \in W))$
3	2	ancomd	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to ((X \in V \land Y \in W) \land Z \in V)$
4		df-3an	$⊢ (X \in V \land Y \in W \land Z \in V) \leftrightarrow ((X \in V \land Y \in W) \land Z \in V)$
5	3 4	sylibr	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to (X \in V \land Y \in W \land Z \in V)$
6		snopfsupp	$⊢ (X \in V \land Y \in W \land Z \in V) \to {finSupp}_{Z} (\{⟨X, Y⟩\})$
7	5 6	syl	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to {finSupp}_{Z} (\{⟨X, Y⟩\})$
8		funsng	$⊢ (X \in V \land Y \in W) \to Fun \{⟨X, Y⟩\}$
9		simpl	$⊢ (Fun F \land X \notin dom F) \to Fun F$
10	8 9	anim12ci	$⊢ ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to (Fun F \land Fun \{⟨X, Y⟩\})$
11		dmsnopg	$⊢ Y \in W \to dom \{⟨X, Y⟩\} = \{X\}$
12	11	adantl	$⊢ (X \in V \land Y \in W) \to dom \{⟨X, Y⟩\} = \{X\}$
13	12	ineq2d	$⊢ (X \in V \land Y \in W) \to dom F \cap dom \{⟨X, Y⟩\} = dom F \cap \{X\}$
14		df-nel	$⊢ X \notin dom F \leftrightarrow \neg X \in dom F$
15		disjsn	$⊢ dom F \cap \{X\} = \emptyset \leftrightarrow \neg X \in dom F$
16	14 15	sylbb2	$⊢ X \notin dom F \to dom F \cap \{X\} = \emptyset$
17	16	adantl	$⊢ (Fun F \land X \notin dom F) \to dom F \cap \{X\} = \emptyset$
18	13 17	sylan9eq	$⊢ ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to dom F \cap dom \{⟨X, Y⟩\} = \emptyset$
19	10 18	jca	$⊢ ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to ((Fun F \land Fun \{⟨X, Y⟩\}) \land dom F \cap dom \{⟨X, Y⟩\} = \emptyset)$
20	19	adantl	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to ((Fun F \land Fun \{⟨X, Y⟩\}) \land dom F \cap dom \{⟨X, Y⟩\} = \emptyset)$
21		funun	$⊢ ((Fun F \land Fun \{⟨X, Y⟩\}) \land dom F \cap dom \{⟨X, Y⟩\} = \emptyset) \to Fun (F \cup \{⟨X, Y⟩\})$
22	20 21	syl	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to Fun (F \cup \{⟨X, Y⟩\})$
23	22	fsuppunbi	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow ({finSupp}_{Z} (F) \land {finSupp}_{Z} (\{⟨X, Y⟩\})))$
24	7 23	mpbiran2d	$⊢ (Z \in V \land ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F))) \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow {finSupp}_{Z} (F))$
25	24	ex	$⊢ Z \in V \to (((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow {finSupp}_{Z} (F)))$
26		relfsupp	$⊢ Rel finSupp$
27	26	brrelex2i	$⊢ {finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \to Z \in V$
28	26	brrelex2i	$⊢ {finSupp}_{Z} (F) \to Z \in V$
29	27 28	pm5.21ni	$⊢ \neg Z \in V \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow {finSupp}_{Z} (F))$
30	29	a1d	$⊢ \neg Z \in V \to (((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow {finSupp}_{Z} (F)))$
31	25 30	pm2.61i	$⊢ ((X \in V \land Y \in W) \land (Fun F \land X \notin dom F)) \to ({finSupp}_{Z} ((F \cup \{⟨X, Y⟩\})) \leftrightarrow {finSupp}_{Z} (F))$

Metamath Proof Explorer

Theorem funsnfsupp

Proof