psss

Description: Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010)

		Ref	Expression
	Assertion	psss	$⊢ R \in PosetRel \to R \cap (A \times A) \in PosetRel$

Proof

Step	Hyp	Ref	Expression
1		inss1	$⊢ R \cap (A \times A) \subseteq R$
2		psrel	$⊢ R \in PosetRel \to Rel R$
3		relss	$⊢ R \cap (A \times A) \subseteq R \to (Rel R \to Rel (R \cap (A \times A)))$
4	1 2 3	mpsyl	$⊢ R \in PosetRel \to Rel (R \cap (A \times A))$
5		pstr2	$⊢ R \in PosetRel \to R \circ R \subseteq R$
6		trinxp	$⊢ R \circ R \subseteq R \to (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \cap (A \times A)$
7	5 6	syl	$⊢ R \in PosetRel \to (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \cap (A \times A)$
8		uniin	$⊢ ⋃ (R \cap (A \times A)) \subseteq ⋃ R \cap ⋃ (A \times A)$
9	8	unissi	$⊢ ⋃ ⋃ (R \cap (A \times A)) \subseteq ⋃ (⋃ R \cap ⋃ (A \times A))$
10		uniin	$⊢ ⋃ (⋃ R \cap ⋃ (A \times A)) \subseteq ⋃ ⋃ R \cap ⋃ ⋃ (A \times A)$
11	9 10	sstri	$⊢ ⋃ ⋃ (R \cap (A \times A)) \subseteq ⋃ ⋃ R \cap ⋃ ⋃ (A \times A)$
12		elin	$⊢ x \in (⋃ ⋃ R \cap ⋃ ⋃ (A \times A)) \leftrightarrow (x \in ⋃ ⋃ R \land x \in ⋃ ⋃ (A \times A))$
13		unixpid	$⊢ ⋃ ⋃ (A \times A) = A$
14	13	eleq2i	$⊢ x \in ⋃ ⋃ (A \times A) \leftrightarrow x \in A$
15		simprr	$⊢ (R \in PosetRel \land (x \in ⋃ ⋃ R \land x \in A)) \to x \in A$
16		psdmrn	$⊢ R \in PosetRel \to (dom R = ⋃ ⋃ R \land ran R = ⋃ ⋃ R)$
17	16	simpld	$⊢ R \in PosetRel \to dom R = ⋃ ⋃ R$
18	17	eleq2d	$⊢ R \in PosetRel \to (x \in dom R \leftrightarrow x \in ⋃ ⋃ R)$
19	18	biimpar	$⊢ (R \in PosetRel \land x \in ⋃ ⋃ R) \to x \in dom R$
20		eqid	$⊢ dom R = dom R$
21	20	psref	$⊢ (R \in PosetRel \land x \in dom R) \to x R x$
22	19 21	syldan	$⊢ (R \in PosetRel \land x \in ⋃ ⋃ R) \to x R x$
23	22	adantrr	$⊢ (R \in PosetRel \land (x \in ⋃ ⋃ R \land x \in A)) \to x R x$
24		brinxp2	$⊢ x (R \cap (A \times A)) x \leftrightarrow ((x \in A \land x \in A) \land x R x)$
25	15 15 23 24	syl21anbrc	$⊢ (R \in PosetRel \land (x \in ⋃ ⋃ R \land x \in A)) \to x (R \cap (A \times A)) x$
26	25	expr	$⊢ (R \in PosetRel \land x \in ⋃ ⋃ R) \to (x \in A \to x (R \cap (A \times A)) x)$
27	14 26	biimtrid	$⊢ (R \in PosetRel \land x \in ⋃ ⋃ R) \to (x \in ⋃ ⋃ (A \times A) \to x (R \cap (A \times A)) x)$
28	27	expimpd	$⊢ R \in PosetRel \to ((x \in ⋃ ⋃ R \land x \in ⋃ ⋃ (A \times A)) \to x (R \cap (A \times A)) x)$
29	12 28	biimtrid	$⊢ R \in PosetRel \to (x \in (⋃ ⋃ R \cap ⋃ ⋃ (A \times A)) \to x (R \cap (A \times A)) x)$
30	29	ralrimiv	$⊢ R \in PosetRel \to \forall x \in (⋃ ⋃ R \cap ⋃ ⋃ (A \times A)) x (R \cap (A \times A)) x$
31		ssralv	$⊢ ⋃ ⋃ (R \cap (A \times A)) \subseteq ⋃ ⋃ R \cap ⋃ ⋃ (A \times A) \to (\forall x \in (⋃ ⋃ R \cap ⋃ ⋃ (A \times A)) x (R \cap (A \times A)) x \to \forall x \in ⋃ ⋃ (R \cap (A \times A)) x (R \cap (A \times A)) x)$
32	11 30 31	mpsyl	$⊢ R \in PosetRel \to \forall x \in ⋃ ⋃ (R \cap (A \times A)) x (R \cap (A \times A)) x$
33	1	ssbri	$⊢ x (R \cap (A \times A)) y \to x R y$
34	1	ssbri	$⊢ y (R \cap (A \times A)) x \to y R x$
35		psasym	$⊢ (R \in PosetRel \land x R y \land y R x) \to x = y$
36	35	3expib	$⊢ R \in PosetRel \to ((x R y \land y R x) \to x = y)$
37	33 34 36	syl2ani	$⊢ R \in PosetRel \to ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) x) \to x = y)$
38	37	alrimivv	$⊢ R \in PosetRel \to \forall x \forall y ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) x) \to x = y)$
39		asymref2	$⊢ (R \cap (A \times A)) \cap {(R \cap (A \times A))}^{-1} = {I ↾}_{⋃ ⋃ (R \cap (A \times A))} \leftrightarrow (\forall x \in ⋃ ⋃ (R \cap (A \times A)) x (R \cap (A \times A)) x \land \forall x \forall y ((x (R \cap (A \times A)) y \land y (R \cap (A \times A)) x) \to x = y))$
40	32 38 39	sylanbrc	$⊢ R \in PosetRel \to (R \cap (A \times A)) \cap {(R \cap (A \times A))}^{-1} = {I ↾}_{⋃ ⋃ (R \cap (A \times A))}$
41		inex1g	$⊢ R \in PosetRel \to R \cap (A \times A) \in V$
42		isps	$⊢ R \cap (A \times A) \in V \to (R \cap (A \times A) \in PosetRel \leftrightarrow (Rel (R \cap (A \times A)) \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \cap (A \times A) \land (R \cap (A \times A)) \cap {(R \cap (A \times A))}^{-1} = {I ↾}_{⋃ ⋃ (R \cap (A \times A))}))$
43	41 42	syl	$⊢ R \in PosetRel \to (R \cap (A \times A) \in PosetRel \leftrightarrow (Rel (R \cap (A \times A)) \land (R \cap (A \times A)) \circ (R \cap (A \times A)) \subseteq R \cap (A \times A) \land (R \cap (A \times A)) \cap {(R \cap (A \times A))}^{-1} = {I ↾}_{⋃ ⋃ (R \cap (A \times A))}))$
44	4 7 40 43	mpbir3and	$⊢ R \in PosetRel \to R \cap (A \times A) \in PosetRel$

Metamath Proof Explorer

Theorem psss

Proof