idsset

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

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

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

Metamath Proof Explorer