tsrss

Description: Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010) (Proof shortened by Mario Carneiro, 21-Nov-2013)

		Ref	Expression
	Assertion	tsrss	$⊢ R \in TosetRel \to R \cap (A \times A) \in TosetRel$

Proof

Step	Hyp	Ref	Expression
1		psss	$⊢ R \in PosetRel \to R \cap (A \times A) \in PosetRel$
2		inss1	$⊢ R \cap (A \times A) \subseteq R$
3		dmss	$⊢ R \cap (A \times A) \subseteq R \to dom (R \cap (A \times A)) \subseteq dom R$
4		ssralv	$⊢ dom (R \cap (A \times A)) \subseteq dom R \to (\forall x \in dom R \forall y \in dom R (x R y \lor y R x) \to \forall x \in dom (R \cap (A \times A)) \forall y \in dom R (x R y \lor y R x))$
5	2 3 4	mp2b	$⊢ \forall x \in dom R \forall y \in dom R (x R y \lor y R x) \to \forall x \in dom (R \cap (A \times A)) \forall y \in dom R (x R y \lor y R x)$
6		ssralv	$⊢ dom (R \cap (A \times A)) \subseteq dom R \to (\forall y \in dom R (x R y \lor y R x) \to \forall y \in dom (R \cap (A \times A)) (x R y \lor y R x))$
7	2 3 6	mp2b	$⊢ \forall y \in dom R (x R y \lor y R x) \to \forall y \in dom (R \cap (A \times A)) (x R y \lor y R x)$
8	7	ralimi	$⊢ \forall x \in dom (R \cap (A \times A)) \forall y \in dom R (x R y \lor y R x) \to \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x R y \lor y R x)$
9	5 8	syl	$⊢ \forall x \in dom R \forall y \in dom R (x R y \lor y R x) \to \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x R y \lor y R x)$
10		inss2	$⊢ R \cap (A \times A) \subseteq A \times A$
11		dmss	$⊢ R \cap (A \times A) \subseteq A \times A \to dom (R \cap (A \times A)) \subseteq dom (A \times A)$
12	10 11	ax-mp	$⊢ dom (R \cap (A \times A)) \subseteq dom (A \times A)$
13		dmxpid	$⊢ dom (A \times A) = A$
14	12 13	sseqtri	$⊢ dom (R \cap (A \times A)) \subseteq A$
15	14	sseli	$⊢ x \in dom (R \cap (A \times A)) \to x \in A$
16	14	sseli	$⊢ y \in dom (R \cap (A \times A)) \to y \in A$
17		brinxp	$⊢ (x \in A \land y \in A) \to (x R y \leftrightarrow x (R \cap (A \times A)) y)$
18		brinxp	$⊢ (y \in A \land x \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
19	18	ancoms	$⊢ (x \in A \land y \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
20	17 19	orbi12d	$⊢ (x \in A \land y \in A) \to ((x R y \lor y R x) \leftrightarrow (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x))$
21	15 16 20	syl2an	$⊢ (x \in dom (R \cap (A \times A)) \land y \in dom (R \cap (A \times A))) \to ((x R y \lor y R x) \leftrightarrow (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x))$
22	21	ralbidva	$⊢ x \in dom (R \cap (A \times A)) \to (\forall y \in dom (R \cap (A \times A)) (x R y \lor y R x) \leftrightarrow \forall y \in dom (R \cap (A \times A)) (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x))$
23	22	ralbiia	$⊢ \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x R y \lor y R x) \leftrightarrow \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x)$
24	9 23	sylib	$⊢ \forall x \in dom R \forall y \in dom R (x R y \lor y R x) \to \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x)$
25	1 24	anim12i	$⊢ (R \in PosetRel \land \forall x \in dom R \forall y \in dom R (x R y \lor y R x)) \to (R \cap (A \times A) \in PosetRel \land \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x))$
26		eqid	$⊢ dom R = dom R$
27	26	istsr2	$⊢ R \in TosetRel \leftrightarrow (R \in PosetRel \land \forall x \in dom R \forall y \in dom R (x R y \lor y R x))$
28		eqid	$⊢ dom (R \cap (A \times A)) = dom (R \cap (A \times A))$
29	28	istsr2	$⊢ R \cap (A \times A) \in TosetRel \leftrightarrow (R \cap (A \times A) \in PosetRel \land \forall x \in dom (R \cap (A \times A)) \forall y \in dom (R \cap (A \times A)) (x (R \cap (A \times A)) y \lor y (R \cap (A \times A)) x))$
30	25 27 29	3imtr4i	$⊢ R \in TosetRel \to R \cap (A \times A) \in TosetRel$

Metamath Proof Explorer

Theorem tsrss

Proof