isps

Description: The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008)

		Ref	Expression
	Assertion	isps	$⊢ R \in A \to (R \in PosetRel \leftrightarrow (Rel R \land R \circ R \subseteq R \land R \cap R^{-1} = {I ↾}_{⋃ ⋃ R}))$

Step	Hyp	Ref	Expression
1		releq	$⊢ r = R \to (Rel r \leftrightarrow Rel R)$
2		coeq1	$⊢ r = R \to r \circ r = R \circ r$
3		coeq2	$⊢ r = R \to R \circ r = R \circ R$
4	2 3	eqtrd	$⊢ r = R \to r \circ r = R \circ R$
5		id	$⊢ r = R \to r = R$
6	4 5	sseq12d	$⊢ r = R \to (r \circ r \subseteq r \leftrightarrow R \circ R \subseteq R)$
7		cnveq	$⊢ r = R \to r^{-1} = R^{-1}$
8	5 7	ineq12d	$⊢ r = R \to r \cap r^{-1} = R \cap R^{-1}$
9		unieq	$⊢ r = R \to ⋃ r = ⋃ R$
10	9	unieqd	$⊢ r = R \to ⋃ ⋃ r = ⋃ ⋃ R$
11	10	reseq2d	$⊢ r = R \to {I ↾}_{⋃ ⋃ r} = {I ↾}_{⋃ ⋃ R}$
12	8 11	eqeq12d	$⊢ r = R \to (r \cap r^{-1} = {I ↾}_{⋃ ⋃ r} \leftrightarrow R \cap R^{-1} = {I ↾}_{⋃ ⋃ R})$
13	1 6 12	3anbi123d	$⊢ r = R \to ((Rel r \land r \circ r \subseteq r \land r \cap r^{-1} = {I ↾}_{⋃ ⋃ r}) \leftrightarrow (Rel R \land R \circ R \subseteq R \land R \cap R^{-1} = {I ↾}_{⋃ ⋃ R}))$
14		df-ps	$⊢ PosetRel = \{r \| (Rel r \land r \circ r \subseteq r \land r \cap r^{-1} = {I ↾}_{⋃ ⋃ r})\}$
15	13 14	elab2g	$⊢ R \in A \to (R \in PosetRel \leftrightarrow (Rel R \land R \circ R \subseteq R \land R \cap R^{-1} = {I ↾}_{⋃ ⋃ R}))$

Metamath Proof Explorer