Theorem resinsnALT

Description: Restriction to the intersection with a singleton. (Contributed by Zhi Wang, 6-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	resinsnALT	$$⊢{F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \neg B\in \left(\mathrm{dom}F\cap A\right)$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)$$
2		reldm0	$$⊢\mathrm{Rel}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)\to \left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\varnothing \right)$$
3	1 2	ax-mp	$$⊢{F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\varnothing$$
4		dmres	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\left(A\cap \left\{B\right\}\right)\cap \mathrm{dom}F$$
5		incom	$$⊢\left(A\cap \left\{B\right\}\right)\cap \mathrm{dom}F=\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)$$
6	4 5	eqtri	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)$$
7	6	eqeq1i	$$⊢\mathrm{dom}\left({F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}\right)=\varnothing \leftrightarrow \mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing$$
8		elin	$$⊢B\in \left(\mathrm{dom}F\cap A\right)\leftrightarrow \left(B\in \mathrm{dom}F\wedge B\in A\right)$$
9		ancom	$$⊢\left(B\in \mathrm{dom}F\wedge B\in A\right)\leftrightarrow \left(B\in A\wedge B\in \mathrm{dom}F\right)$$
10		snssi	$$⊢B\in A\to \left\{B\right\}\subseteq A$$
11		incom	$$⊢A\cap \left\{B\right\}=\left\{B\right\}\cap A$$
12		dfss2	$$⊢\left\{B\right\}\subseteq A\leftrightarrow \left\{B\right\}\cap A=\left\{B\right\}$$
13	12	biimpi	$$⊢\left\{B\right\}\subseteq A\to \left\{B\right\}\cap A=\left\{B\right\}$$
14	11 13	eqtrid	$$⊢\left\{B\right\}\subseteq A\to A\cap \left\{B\right\}=\left\{B\right\}$$
15	10 14	syl	$$⊢B\in A\to A\cap \left\{B\right\}=\left\{B\right\}$$
16	15	ineq2d	$$⊢B\in A\to \mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\mathrm{dom}F\cap \left\{B\right\}$$
17	16	eqeq1d	$$⊢B\in A\to \left(\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing \leftrightarrow \mathrm{dom}F\cap \left\{B\right\}=\varnothing \right)$$
18		disjsn	$$⊢\mathrm{dom}F\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in \mathrm{dom}F$$
19	17 18	bitrdi	$$⊢B\in A\to \left(\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing \leftrightarrow \neg B\in \mathrm{dom}F\right)$$
20		disjsn	$$⊢A\cap \left\{B\right\}=\varnothing \leftrightarrow \neg B\in A$$
21	20	biimpri	$$⊢\neg B\in A\to A\cap \left\{B\right\}=\varnothing$$
22	21	ineq2d	$$⊢\neg B\in A\to \mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\mathrm{dom}F\cap \varnothing$$
23		in0	$$⊢\mathrm{dom}F\cap \varnothing =\varnothing$$
24	22 23	eqtrdi	$$⊢\neg B\in A\to \mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing$$
25	19 24	resinsnlem	$$⊢\left(B\in A\wedge B\in \mathrm{dom}F\right)\leftrightarrow \neg \mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing$$
26	8 9 25	3bitri	$$⊢B\in \left(\mathrm{dom}F\cap A\right)\leftrightarrow \neg \mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing$$
27	26	con2bii	$$⊢\mathrm{dom}F\cap \left(A\cap \left\{B\right\}\right)=\varnothing \leftrightarrow \neg B\in \left(\mathrm{dom}F\cap A\right)$$
28	3 7 27	3bitri	$$⊢{F\upharpoonright }_{\left(A\cap \left\{B\right\}\right)}=\varnothing \leftrightarrow \neg B\in \left(\mathrm{dom}F\cap A\right)$$