suppimacnv

Description: Support sets of functions expressed by inverse images. (Contributed by AV, 31-Mar-2019) (Revised by AV, 7-Apr-2019)

		Ref	Expression
	Assertion	suppimacnv	$⊢ (R \in V \land Z \in W) \to R supp Z = R^{-1} [V ∖ \{Z\}]$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ t = s \to (x R t \leftrightarrow x R s)$
2	1	cbvexvw	$⊢ \exists t x R t \leftrightarrow \exists s x R s$
3		breq2	$⊢ s = Z \to (x R s \leftrightarrow x R Z)$
4	3	anbi1d	$⊢ s = Z \to ((x R s \land (x R t \leftrightarrow t \neq Z)) \leftrightarrow (x R Z \land (x R t \leftrightarrow t \neq Z)))$
5		bianir	$⊢ (t \neq Z \land (x R t \leftrightarrow t \neq Z)) \to x R t$
6		vex	$⊢ t \in V$
7		breq2	$⊢ y = t \to (x R y \leftrightarrow x R t)$
8		neeq1	$⊢ y = t \to (y \neq Z \leftrightarrow t \neq Z)$
9	7 8	anbi12d	$⊢ y = t \to ((x R y \land y \neq Z) \leftrightarrow (x R t \land t \neq Z))$
10	6 9	spcev	$⊢ (x R t \land t \neq Z) \to \exists y (x R y \land y \neq Z)$
11	10	ex	$⊢ x R t \to (t \neq Z \to \exists y (x R y \land y \neq Z))$
12	5 11	syl	$⊢ (t \neq Z \land (x R t \leftrightarrow t \neq Z)) \to (t \neq Z \to \exists y (x R y \land y \neq Z))$
13	12	ex	$⊢ t \neq Z \to ((x R t \leftrightarrow t \neq Z) \to (t \neq Z \to \exists y (x R y \land y \neq Z)))$
14	13	pm2.43a	$⊢ t \neq Z \to ((x R t \leftrightarrow t \neq Z) \to \exists y (x R y \land y \neq Z))$
15	14	adantld	$⊢ t \neq Z \to ((x R Z \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z))$
16		nne	$⊢ \neg t \neq Z \leftrightarrow t = Z$
17		notbi	$⊢ (x R t \leftrightarrow t \neq Z) \leftrightarrow (\neg x R t \leftrightarrow \neg t \neq Z)$
18		bianir	$⊢ (\neg t \neq Z \land (\neg x R t \leftrightarrow \neg t \neq Z)) \to \neg x R t$
19		breq2	$⊢ Z = t \to (x R Z \leftrightarrow x R t)$
20	19	eqcoms	$⊢ t = Z \to (x R Z \leftrightarrow x R t)$
21		pm2.24	$⊢ x R t \to (\neg x R t \to \exists y (x R y \land y \neq Z))$
22	20 21	biimtrdi	$⊢ t = Z \to (x R Z \to (\neg x R t \to \exists y (x R y \land y \neq Z)))$
23	22	com13	$⊢ \neg x R t \to (x R Z \to (t = Z \to \exists y (x R y \land y \neq Z)))$
24	18 23	syl	$⊢ (\neg t \neq Z \land (\neg x R t \leftrightarrow \neg t \neq Z)) \to (x R Z \to (t = Z \to \exists y (x R y \land y \neq Z)))$
25	24	ex	$⊢ \neg t \neq Z \to ((\neg x R t \leftrightarrow \neg t \neq Z) \to (x R Z \to (t = Z \to \exists y (x R y \land y \neq Z))))$
26	17 25	biimtrid	$⊢ \neg t \neq Z \to ((x R t \leftrightarrow t \neq Z) \to (x R Z \to (t = Z \to \exists y (x R y \land y \neq Z))))$
27	26	com13	$⊢ x R Z \to ((x R t \leftrightarrow t \neq Z) \to (\neg t \neq Z \to (t = Z \to \exists y (x R y \land y \neq Z))))$
28	27	imp	$⊢ (x R Z \land (x R t \leftrightarrow t \neq Z)) \to (\neg t \neq Z \to (t = Z \to \exists y (x R y \land y \neq Z)))$
29	28	com13	$⊢ t = Z \to (\neg t \neq Z \to ((x R Z \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z)))$
30	16 29	sylbi	$⊢ \neg t \neq Z \to (\neg t \neq Z \to ((x R Z \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z)))$
31	30	pm2.43i	$⊢ \neg t \neq Z \to ((x R Z \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z))$
32	15 31	pm2.61i	$⊢ (x R Z \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z)$
33	4 32	biimtrdi	$⊢ s = Z \to ((x R s \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z))$
34		vex	$⊢ s \in V$
35		breq2	$⊢ y = s \to (x R y \leftrightarrow x R s)$
36		neeq1	$⊢ y = s \to (y \neq Z \leftrightarrow s \neq Z)$
37	35 36	anbi12d	$⊢ y = s \to ((x R y \land y \neq Z) \leftrightarrow (x R s \land s \neq Z))$
38	34 37	spcev	$⊢ (x R s \land s \neq Z) \to \exists y (x R y \land y \neq Z)$
39	38	ex	$⊢ x R s \to (s \neq Z \to \exists y (x R y \land y \neq Z))$
40	39	adantr	$⊢ (x R s \land (x R t \leftrightarrow t \neq Z)) \to (s \neq Z \to \exists y (x R y \land y \neq Z))$
41	40	com12	$⊢ s \neq Z \to ((x R s \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z))$
42	33 41	pm2.61ine	$⊢ (x R s \land (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z)$
43	42	expcom	$⊢ (x R t \leftrightarrow t \neq Z) \to (x R s \to \exists y (x R y \land y \neq Z))$
44	43	exlimiv	$⊢ \exists t (x R t \leftrightarrow t \neq Z) \to (x R s \to \exists y (x R y \land y \neq Z))$
45	44	com12	$⊢ x R s \to (\exists t (x R t \leftrightarrow t \neq Z) \to \exists y (x R y \land y \neq Z))$
46	45	exlimiv	$⊢ \exists s x R s \to (\exists t (x R t \leftrightarrow t \neq Z) \to \exists y (x R y \land y \neq Z))$
47	2 46	sylbi	$⊢ \exists t x R t \to (\exists t (x R t \leftrightarrow t \neq Z) \to \exists y (x R y \land y \neq Z))$
48	47	imp	$⊢ (\exists t x R t \land \exists t (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z)$
49	48	a1i	$⊢ (R \in V \land Z \in W) \to ((\exists t x R t \land \exists t (x R t \leftrightarrow t \neq Z)) \to \exists y (x R y \land y \neq Z))$
50	49	ss2abdv	$⊢ (R \in V \land Z \in W) \to \{x \| (\exists t x R t \land \exists t (x R t \leftrightarrow t \neq Z))\} \subseteq \{x \| \exists y (x R y \land y \neq Z)\}$
51		suppvalbr	$⊢ (R \in V \land Z \in W) \to R supp Z = \{x \| (\exists t x R t \land \exists t (x R t \leftrightarrow t \neq Z))\}$
52		cnvimadfsn	$⊢ R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (x R y \land y \neq Z)\}$
53	52	a1i	$⊢ (R \in V \land Z \in W) \to R^{-1} [V ∖ \{Z\}] = \{x \| \exists y (x R y \land y \neq Z)\}$
54	50 51 53	3sstr4d	$⊢ (R \in V \land Z \in W) \to R supp Z \subseteq R^{-1} [V ∖ \{Z\}]$
55		suppimacnvss	$⊢ (R \in V \land Z \in W) \to R^{-1} [V ∖ \{Z\}] \subseteq R supp Z$
56	54 55	eqssd	$⊢ (R \in V \land Z \in W) \to R supp Z = R^{-1} [V ∖ \{Z\}]$

Metamath Proof Explorer

Theorem suppimacnv

Proof