resspos

Description: The restriction of a Poset is a Poset. (Contributed by Thierry Arnoux, 20-Jan-2018)

		Ref	Expression
	Assertion	resspos	$⊢ (F \in Poset \land A \in V) \to F ↾_{𝑠} A \in Poset$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ (F \in Poset \land A \in V) \to F ↾_{𝑠} A \in V$
2		eqid	$⊢ F ↾_{𝑠} A = F ↾_{𝑠} A$
3		eqid	$⊢ {Base}_{F} = {Base}_{F}$
4	2 3	ressbas	$⊢ A \in V \to A \cap {Base}_{F} = {Base}_{(F ↾_{𝑠} A)}$
5		inss2	$⊢ A \cap {Base}_{F} \subseteq {Base}_{F}$
6	4 5	eqsstrrdi	$⊢ A \in V \to {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F}$
7	6	adantl	$⊢ (F \in Poset \land A \in V) \to {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F}$
8		eqid	$⊢ \leq_{F} = \leq_{F}$
9	3 8	ispos	$⊢ F \in Poset \leftrightarrow (F \in V \land \forall x \in {Base}_{F} \forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
10	9	simprbi	$⊢ F \in Poset \to \forall x \in {Base}_{F} \forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z))$
11	10	adantr	$⊢ (F \in Poset \land A \in V) \to \forall x \in {Base}_{F} \forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z))$
12		ssralv	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
13	12	ralimdv	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall y \in {Base}_{F} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
14		ssralv	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall y \in {Base}_{F} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
15	13 14	syld	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
16	15	ralimdv	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall x \in {Base}_{F} \forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall x \in {Base}_{F} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
17		ssralv	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall x \in {Base}_{F} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
18	16 17	syld	$⊢ {Base}_{(F ↾_{𝑠} A)} \subseteq {Base}_{F} \to (\forall x \in {Base}_{F} \forall y \in {Base}_{F} \forall z \in {Base}_{F} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \to \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)))$
19	7 11 18	sylc	$⊢ (F \in Poset \land A \in V) \to \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z))$
20	2 8	ressle	$⊢ A \in V \to \leq_{F} = \leq_{(F ↾_{𝑠} A)}$
21	20	adantl	$⊢ (F \in Poset \land A \in V) \to \leq_{F} = \leq_{(F ↾_{𝑠} A)}$
22		breq	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (x \leq_{F} x \leftrightarrow x \leq_{(F ↾_{𝑠} A)} x)$
23		breq	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (x \leq_{F} y \leftrightarrow x \leq_{(F ↾_{𝑠} A)} y)$
24		breq	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (y \leq_{F} x \leftrightarrow y \leq_{(F ↾_{𝑠} A)} x)$
25	23 24	anbi12d	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to ((x \leq_{F} y \land y \leq_{F} x) \leftrightarrow (x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x))$
26	25	imbi1d	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (((x \leq_{F} y \land y \leq_{F} x) \to x = y) \leftrightarrow ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y))$
27		breq	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (y \leq_{F} z \leftrightarrow y \leq_{(F ↾_{𝑠} A)} z)$
28	23 27	anbi12d	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to ((x \leq_{F} y \land y \leq_{F} z) \leftrightarrow (x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z))$
29		breq	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (x \leq_{F} z \leftrightarrow x \leq_{(F ↾_{𝑠} A)} z)$
30	28 29	imbi12d	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z) \leftrightarrow ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z))$
31	22 26 30	3anbi123d	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to ((x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \leftrightarrow (x \leq_{(F ↾_{𝑠} A)} x \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y) \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z)))$
32	31	ralbidv	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (\forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \leftrightarrow \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{(F ↾_{𝑠} A)} x \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y) \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z)))$
33	32	2ralbidv	$⊢ \leq_{F} = \leq_{(F ↾_{𝑠} A)} \to (\forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \leftrightarrow \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{(F ↾_{𝑠} A)} x \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y) \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z)))$
34	21 33	syl	$⊢ (F \in Poset \land A \in V) \to (\forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{F} x \land ((x \leq_{F} y \land y \leq_{F} x) \to x = y) \land ((x \leq_{F} y \land y \leq_{F} z) \to x \leq_{F} z)) \leftrightarrow \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{(F ↾_{𝑠} A)} x \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y) \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z)))$
35	19 34	mpbid	$⊢ (F \in Poset \land A \in V) \to \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{(F ↾_{𝑠} A)} x \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y) \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z))$
36		eqid	$⊢ {Base}_{(F ↾_{𝑠} A)} = {Base}_{(F ↾_{𝑠} A)}$
37		eqid	$⊢ \leq_{(F ↾_{𝑠} A)} = \leq_{(F ↾_{𝑠} A)}$
38	36 37	ispos	$⊢ F ↾_{𝑠} A \in Poset \leftrightarrow (F ↾_{𝑠} A \in V \land \forall x \in {Base}_{(F ↾_{𝑠} A)} \forall y \in {Base}_{(F ↾_{𝑠} A)} \forall z \in {Base}_{(F ↾_{𝑠} A)} (x \leq_{(F ↾_{𝑠} A)} x \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} x) \to x = y) \land ((x \leq_{(F ↾_{𝑠} A)} y \land y \leq_{(F ↾_{𝑠} A)} z) \to x \leq_{(F ↾_{𝑠} A)} z)))$
39	1 35 38	sylanbrc	$⊢ (F \in Poset \land A \in V) \to F ↾_{𝑠} A \in Poset$

Metamath Proof Explorer

Theorem resspos

Proof