Theorem idsset

Description: _I is equal to the intersection of SSet and its converse. (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	idsset	$$⊢\mathrm{I}=\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
2		relsset	$$⊢\mathrm{Rel}\mathrm{𝖲𝖲𝖾𝗍}$$
3		relin1	$$⊢\mathrm{Rel}\mathrm{𝖲𝖲𝖾𝗍}\to \mathrm{Rel}\left(\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\right)$$
4	2 3	ax-mp	$$⊢\mathrm{Rel}\left(\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\right)$$
5		eqss	$$⊢y=z\leftrightarrow \left(y\subseteq z\wedge z\subseteq y\right)$$
6		vex	$$⊢z\in \mathrm{V}$$
7	6	ideq	$$⊢y\mathrm{I}z\leftrightarrow y=z$$
8		brin	$$⊢y\left(\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\right)z\leftrightarrow \left(y\mathrm{𝖲𝖲𝖾𝗍}z\wedge y{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}z\right)$$
9	6	brsset	$$⊢y\mathrm{𝖲𝖲𝖾𝗍}z\leftrightarrow y\subseteq z$$
10		vex	$$⊢y\in \mathrm{V}$$
11	10 6	brcnv	$$⊢y{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}z\leftrightarrow z\mathrm{𝖲𝖲𝖾𝗍}y$$
12	10	brsset	$$⊢z\mathrm{𝖲𝖲𝖾𝗍}y\leftrightarrow z\subseteq y$$
13	11 12	bitri	$$⊢y{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}z\leftrightarrow z\subseteq y$$
14	9 13	anbi12i	$$⊢\left(y\mathrm{𝖲𝖲𝖾𝗍}z\wedge y{\mathrm{𝖲𝖲𝖾𝗍}}^{-1}z\right)\leftrightarrow \left(y\subseteq z\wedge z\subseteq y\right)$$
15	8 14	bitri	$$⊢y\left(\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\right)z\leftrightarrow \left(y\subseteq z\wedge z\subseteq y\right)$$
16	5 7 15	3bitr4i	$$⊢y\mathrm{I}z\leftrightarrow y\left(\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}\right)z$$
17	1 4 16	eqbrriv	$$⊢\mathrm{I}=\mathrm{𝖲𝖲𝖾𝗍}\cap {\mathrm{𝖲𝖲𝖾𝗍}}^{-1}$$