Metamath Proof Explorer

Theorem cosscnvssid3

Description: Equivalent expressions for the class of cosets by the converse of R to be a subset of the identity class. (Contributed by Peter Mazsa, 28-Jul-2021)

		Ref	Expression
	Assertion	cosscnvssid3	$⊢ ≀ R^{-1} \subseteq I \leftrightarrow \forall u \forall v \forall x ((u R x \land v R x) \to u = v)$

Proof

Step	Hyp	Ref	Expression
1		cossssid3	$⊢ ≀ R^{-1} \subseteq I \leftrightarrow \forall x \forall u \forall v ((x R^{-1} u \land x R^{-1} v) \to u = v)$
2		alrot3	$⊢ \forall x \forall u \forall v ((x R^{-1} u \land x R^{-1} v) \to u = v) \leftrightarrow \forall u \forall v \forall x ((x R^{-1} u \land x R^{-1} v) \to u = v)$
3		brcnvg	$⊢ (x \in V \land u \in V) \to (x R^{-1} u \leftrightarrow u R x)$
4	3	el2v	$⊢ x R^{-1} u \leftrightarrow u R x$
5		brcnvg	$⊢ (x \in V \land v \in V) \to (x R^{-1} v \leftrightarrow v R x)$
6	5	el2v	$⊢ x R^{-1} v \leftrightarrow v R x$
7	4 6	anbi12i	$⊢ (x R^{-1} u \land x R^{-1} v) \leftrightarrow (u R x \land v R x)$
8	7	imbi1i	$⊢ ((x R^{-1} u \land x R^{-1} v) \to u = v) \leftrightarrow ((u R x \land v R x) \to u = v)$
9	8	3albii	$⊢ \forall u \forall v \forall x ((x R^{-1} u \land x R^{-1} v) \to u = v) \leftrightarrow \forall u \forall v \forall x ((u R x \land v R x) \to u = v)$
10	1 2 9	3bitri	$⊢ ≀ R^{-1} \subseteq I \leftrightarrow \forall u \forall v \forall x ((u R x \land v R x) \to u = v)$