suppsnop

Description: The support of a singleton of an ordered pair. (Contributed by AV, 12-Apr-2019)

		Ref	Expression
	Hypothesis	suppsnop.f	$⊢ F = \{⟨X, Y⟩\}$
	Assertion	suppsnop	$⊢ (X \in V \land Y \in W \land Z \in U) \to F supp Z = if (Y = Z, \emptyset, \{X\})$

Proof

Step	Hyp	Ref	Expression
1		suppsnop.f	$⊢ F = \{⟨X, Y⟩\}$
2		f1osng	$⊢ (X \in V \land Y \in W) \to \{⟨X, Y⟩\} : \{X\} \underset{1-1 onto}{⟶} \{Y\}$
3		f1of	$⊢ \{⟨X, Y⟩\} : \{X\} \underset{1-1 onto}{⟶} \{Y\} \to \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}$
4	2 3	syl	$⊢ (X \in V \land Y \in W) \to \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}$
5	4	3adant3	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}$
6	1	feq1i	$⊢ F : \{X\} ⟶ \{Y\} \leftrightarrow \{⟨X, Y⟩\} : \{X\} ⟶ \{Y\}$
7	5 6	sylibr	$⊢ (X \in V \land Y \in W \land Z \in U) \to F : \{X\} ⟶ \{Y\}$
8		snex	$⊢ \{X\} \in V$
9		fex	$⊢ (F : \{X\} ⟶ \{Y\} \land \{X\} \in V) \to F \in V$
10	7 8 9	sylancl	$⊢ (X \in V \land Y \in W \land Z \in U) \to F \in V$
11		simp3	$⊢ (X \in V \land Y \in W \land Z \in U) \to Z \in U$
12		suppval	$⊢ (F \in V \land Z \in U) \to F supp Z = \{x \in dom F \| F [\{x\}] \neq \{Z\}\}$
13	10 11 12	syl2anc	$⊢ (X \in V \land Y \in W \land Z \in U) \to F supp Z = \{x \in dom F \| F [\{x\}] \neq \{Z\}\}$
14	7	fdmd	$⊢ (X \in V \land Y \in W \land Z \in U) \to dom F = \{X\}$
15	14	rabeqdv	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{x \in dom F \| F [\{x\}] \neq \{Z\}\} = \{x \in \{X\} \| F [\{x\}] \neq \{Z\}\}$
16		sneq	$⊢ x = X \to \{x\} = \{X\}$
17	16	imaeq2d	$⊢ x = X \to F [\{x\}] = F [\{X\}]$
18	17	neeq1d	$⊢ x = X \to (F [\{x\}] \neq \{Z\} \leftrightarrow F [\{X\}] \neq \{Z\})$
19	18	rabsnif	$⊢ \{x \in \{X\} \| F [\{x\}] \neq \{Z\}\} = if (F [\{X\}] \neq \{Z\}, \{X\}, \emptyset)$
20	15 19	eqtrdi	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{x \in dom F \| F [\{x\}] \neq \{Z\}\} = if (F [\{X\}] \neq \{Z\}, \{X\}, \emptyset)$
21	7	ffnd	$⊢ (X \in V \land Y \in W \land Z \in U) \to F Fn \{X\}$
22		snidg	$⊢ X \in V \to X \in \{X\}$
23	22	3ad2ant1	$⊢ (X \in V \land Y \in W \land Z \in U) \to X \in \{X\}$
24		fnsnfv	$⊢ (F Fn \{X\} \land X \in \{X\}) \to \{F (X)\} = F [\{X\}]$
25	24	eqcomd	$⊢ (F Fn \{X\} \land X \in \{X\}) \to F [\{X\}] = \{F (X)\}$
26	21 23 25	syl2anc	$⊢ (X \in V \land Y \in W \land Z \in U) \to F [\{X\}] = \{F (X)\}$
27	26	neeq1d	$⊢ (X \in V \land Y \in W \land Z \in U) \to (F [\{X\}] \neq \{Z\} \leftrightarrow \{F (X)\} \neq \{Z\})$
28	1	fveq1i	$⊢ F (X) = \{⟨X, Y⟩\} (X)$
29		fvsng	$⊢ (X \in V \land Y \in W) \to \{⟨X, Y⟩\} (X) = Y$
30	29	3adant3	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{⟨X, Y⟩\} (X) = Y$
31	28 30	eqtrid	$⊢ (X \in V \land Y \in W \land Z \in U) \to F (X) = Y$
32	31	sneqd	$⊢ (X \in V \land Y \in W \land Z \in U) \to \{F (X)\} = \{Y\}$
33	32	neeq1d	$⊢ (X \in V \land Y \in W \land Z \in U) \to (\{F (X)\} \neq \{Z\} \leftrightarrow \{Y\} \neq \{Z\})$
34		sneqbg	$⊢ Y \in W \to (\{Y\} = \{Z\} \leftrightarrow Y = Z)$
35	34	3ad2ant2	$⊢ (X \in V \land Y \in W \land Z \in U) \to (\{Y\} = \{Z\} \leftrightarrow Y = Z)$
36	35	necon3abid	$⊢ (X \in V \land Y \in W \land Z \in U) \to (\{Y\} \neq \{Z\} \leftrightarrow \neg Y = Z)$
37	27 33 36	3bitrd	$⊢ (X \in V \land Y \in W \land Z \in U) \to (F [\{X\}] \neq \{Z\} \leftrightarrow \neg Y = Z)$
38	37	ifbid	$⊢ (X \in V \land Y \in W \land Z \in U) \to if (F [\{X\}] \neq \{Z\}, \{X\}, \emptyset) = if (\neg Y = Z, \{X\}, \emptyset)$
39		ifnot	$⊢ if (\neg Y = Z, \{X\}, \emptyset) = if (Y = Z, \emptyset, \{X\})$
40	38 39	eqtrdi	$⊢ (X \in V \land Y \in W \land Z \in U) \to if (F [\{X\}] \neq \{Z\}, \{X\}, \emptyset) = if (Y = Z, \emptyset, \{X\})$
41	13 20 40	3eqtrd	$⊢ (X \in V \land Y \in W \land Z \in U) \to F supp Z = if (Y = Z, \emptyset, \{X\})$

Metamath Proof Explorer

Theorem suppsnop

Proof