Theorem imagesset

Description: The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018)

	Ref	Expression
Assertion	imagesset	$$⊢\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\subseteq \mathrm{𝖲𝖲𝖾𝗍}$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢y\subseteq y$$
2		sseq2	$$⊢z=y\to \left(y\subseteq z\leftrightarrow y\subseteq y\right)$$
3	2	rspcev	$$⊢\left(y\in x\wedge y\subseteq y\right)\to \exists z\in xy\subseteq z$$
4	1 3	mpan2	$$⊢y\in x\to \exists z\in xy\subseteq z$$
5		vex	$$⊢y\in \mathrm{V}$$
6	5	elima	$$⊢y\in {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]\leftrightarrow \exists z\in xz{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}y$$
7		vex	$$⊢z\in \mathrm{V}$$
8	7 5	brcnv	$$⊢z{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}y\leftrightarrow y\mathrm{𝖲𝖲𝖾𝗍}z$$
9	7	brsset	$$⊢y\mathrm{𝖲𝖲𝖾𝗍}z\leftrightarrow y\subseteq z$$
10	8 9	bitri	$$⊢z{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}y\leftrightarrow y\subseteq z$$
11	10	rexbii	$$⊢\exists z\in xz{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}y\leftrightarrow \exists z\in xy\subseteq z$$
12	6 11	bitri	$$⊢y\in {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]\leftrightarrow \exists z\in xy\subseteq z$$
13	4 12	sylibr	$$⊢y\in x\to y\in {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]$$
14	13	ssriv	$$⊢x\subseteq {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]$$
15		sseq2	$$⊢y={\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]\to \left(x\subseteq y\leftrightarrow x\subseteq {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]\right)$$
16	14 15	mpbiri	$$⊢y={\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]\to x\subseteq y$$
17		vex	$$⊢x\in \mathrm{V}$$
18	17 5	brimage	$$⊢x\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}y\leftrightarrow y={\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]$$
19		df-br	$$⊢x\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}y\leftrightarrow ⟨x,y⟩\in \mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}$$
20	18 19	bitr3i	$$⊢y={\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\left[x\right]\leftrightarrow ⟨x,y⟩\in \mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}$$
21	5	brsset	$$⊢x\mathrm{𝖲𝖲𝖾𝗍}y\leftrightarrow x\subseteq y$$
22		df-br	$$⊢x\mathrm{𝖲𝖲𝖾𝗍}y\leftrightarrow ⟨x,y⟩\in \mathrm{𝖲𝖲𝖾𝗍}$$
23	21 22	bitr3i	$$⊢x\subseteq y\leftrightarrow ⟨x,y⟩\in \mathrm{𝖲𝖲𝖾𝗍}$$
24	16 20 23	3imtr3i	$$⊢⟨x,y⟩\in \mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\to ⟨x,y⟩\in \mathrm{𝖲𝖲𝖾𝗍}$$
25	24	gen2	$$⊢\forall x\forall y\left(⟨x,y⟩\in \mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\to ⟨x,y⟩\in \mathrm{𝖲𝖲𝖾𝗍}\right)$$
26		funimage	$$⊢\mathrm{Fun}\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}$$
27		funrel	$$⊢\mathrm{Fun}\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\to \mathrm{Rel}\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}$$
28		ssrel	$$⊢\mathrm{Rel}\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\to \left(\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\subseteq \mathrm{𝖲𝖲𝖾𝗍}\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in \mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\to ⟨x,y⟩\in \mathrm{𝖲𝖲𝖾𝗍}\right)\right)$$
29	26 27 28	mp2b	$$⊢\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\subseteq \mathrm{𝖲𝖲𝖾𝗍}\leftrightarrow \forall x\forall y\left(⟨x,y⟩\in \mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\to ⟨x,y⟩\in \mathrm{𝖲𝖲𝖾𝗍}\right)$$
30	25 29	mpbir	$$⊢\mathrm{𝖨𝗆𝖺𝗀𝖾}{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\subseteq \mathrm{𝖲𝖲𝖾𝗍}$$