ressprs

Description: The restriction of a proset is a proset. (Contributed by Thierry Arnoux, 11-Sep-2015)

		Ref	Expression
	Hypothesis	ressprs.b	$⊢ B = {Base}_{K}$
	Assertion	ressprs	$⊢ (K \in Proset \land A \subseteq B) \to K ↾_{𝑠} A \in Proset$

Proof

Step	Hyp	Ref	Expression
1		ressprs.b	$⊢ B = {Base}_{K}$
2		ovexd	$⊢ (K \in Proset \land A \subseteq B) \to K ↾_{𝑠} A \in V$
3		simp-4l	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to K \in Proset$
4		simp-4r	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to A \subseteq B$
5		simpllr	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to x \in A$
6	4 5	sseldd	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to x \in B$
7	3 6	jca	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to (K \in Proset \land x \in B)$
8		simplr	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to y \in A$
9	4 8	sseldd	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to y \in B$
10		simpr	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to z \in A$
11	4 10	sseldd	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to z \in B$
12		eqid	$⊢ \leq_{K} = \leq_{K}$
13	1 12	isprs	$⊢ K \in Proset \leftrightarrow (K \in V \land \forall x \in B \forall y \in B \forall z \in B (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
14	13	simprbi	$⊢ K \in Proset \to \forall x \in B \forall y \in B \forall z \in B (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
15	14	r19.21bi	$⊢ (K \in Proset \land x \in B) \to \forall y \in B \forall z \in B (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
16	15	r19.21bi	$⊢ ((K \in Proset \land x \in B) \land y \in B) \to \forall z \in B (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
17	16	r19.21bi	$⊢ (((K \in Proset \land x \in B) \land y \in B) \land z \in B) \to (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
18	7 9 11 17	syl21anc	$⊢ ((((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \land z \in A) \to (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
19	18	ralrimiva	$⊢ (((K \in Proset \land A \subseteq B) \land x \in A) \land y \in A) \to \forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
20	19	ralrimiva	$⊢ ((K \in Proset \land A \subseteq B) \land x \in A) \to \forall y \in A \forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
21	20	ralrimiva	$⊢ (K \in Proset \land A \subseteq B) \to \forall x \in A \forall y \in A \forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
22		eqid	$⊢ K ↾_{𝑠} A = K ↾_{𝑠} A$
23	22 1	ressbas2	$⊢ A \subseteq B \to A = {Base}_{(K ↾_{𝑠} A)}$
24	23	adantl	$⊢ (K \in Proset \land A \subseteq B) \to A = {Base}_{(K ↾_{𝑠} A)}$
25	1	fvexi	$⊢ B \in V$
26	25	ssex	$⊢ A \subseteq B \to A \in V$
27	22 12	ressle	$⊢ A \in V \to \leq_{K} = \leq_{(K ↾_{𝑠} A)}$
28	26 27	syl	$⊢ A \subseteq B \to \leq_{K} = \leq_{(K ↾_{𝑠} A)}$
29	28	adantl	$⊢ (K \in Proset \land A \subseteq B) \to \leq_{K} = \leq_{(K ↾_{𝑠} A)}$
30	29	breqd	$⊢ (K \in Proset \land A \subseteq B) \to (x \leq_{K} x \leftrightarrow x \leq_{(K ↾_{𝑠} A)} x)$
31	29	breqd	$⊢ (K \in Proset \land A \subseteq B) \to (x \leq_{K} y \leftrightarrow x \leq_{(K ↾_{𝑠} A)} y)$
32	29	breqd	$⊢ (K \in Proset \land A \subseteq B) \to (y \leq_{K} z \leftrightarrow y \leq_{(K ↾_{𝑠} A)} z)$
33	31 32	anbi12d	$⊢ (K \in Proset \land A \subseteq B) \to ((x \leq_{K} y \land y \leq_{K} z) \leftrightarrow (x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z))$
34	29	breqd	$⊢ (K \in Proset \land A \subseteq B) \to (x \leq_{K} z \leftrightarrow x \leq_{(K ↾_{𝑠} A)} z)$
35	33 34	imbi12d	$⊢ (K \in Proset \land A \subseteq B) \to (((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z) \leftrightarrow ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z))$
36	30 35	anbi12d	$⊢ (K \in Proset \land A \subseteq B) \to ((x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)) \leftrightarrow (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z)))$
37	24 36	raleqbidv	$⊢ (K \in Proset \land A \subseteq B) \to (\forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)) \leftrightarrow \forall z \in {Base}_{(K ↾_{𝑠} A)} (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z)))$
38	24 37	raleqbidv	$⊢ (K \in Proset \land A \subseteq B) \to (\forall y \in A \forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)) \leftrightarrow \forall y \in {Base}_{(K ↾_{𝑠} A)} \forall z \in {Base}_{(K ↾_{𝑠} A)} (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z)))$
39	24 38	raleqbidv	$⊢ (K \in Proset \land A \subseteq B) \to (\forall x \in A \forall y \in A \forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)) \leftrightarrow \forall x \in {Base}_{(K ↾_{𝑠} A)} \forall y \in {Base}_{(K ↾_{𝑠} A)} \forall z \in {Base}_{(K ↾_{𝑠} A)} (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z)))$
40	39	anbi2d	$⊢ (K \in Proset \land A \subseteq B) \to ((K ↾_{𝑠} A \in V \land \forall x \in A \forall y \in A \forall z \in A (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))) \leftrightarrow (K ↾_{𝑠} A \in V \land \forall x \in {Base}_{(K ↾_{𝑠} A)} \forall y \in {Base}_{(K ↾_{𝑠} A)} \forall z \in {Base}_{(K ↾_{𝑠} A)} (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z))))$
41	2 21 40	mpbi2and	$⊢ (K \in Proset \land A \subseteq B) \to (K ↾_{𝑠} A \in V \land \forall x \in {Base}_{(K ↾_{𝑠} A)} \forall y \in {Base}_{(K ↾_{𝑠} A)} \forall z \in {Base}_{(K ↾_{𝑠} A)} (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z)))$
42		eqid	$⊢ {Base}_{(K ↾_{𝑠} A)} = {Base}_{(K ↾_{𝑠} A)}$
43		eqid	$⊢ \leq_{(K ↾_{𝑠} A)} = \leq_{(K ↾_{𝑠} A)}$
44	42 43	isprs	$⊢ K ↾_{𝑠} A \in Proset \leftrightarrow (K ↾_{𝑠} A \in V \land \forall x \in {Base}_{(K ↾_{𝑠} A)} \forall y \in {Base}_{(K ↾_{𝑠} A)} \forall z \in {Base}_{(K ↾_{𝑠} A)} (x \leq_{(K ↾_{𝑠} A)} x \land ((x \leq_{(K ↾_{𝑠} A)} y \land y \leq_{(K ↾_{𝑠} A)} z) \to x \leq_{(K ↾_{𝑠} A)} z)))$
45	41 44	sylibr	$⊢ (K \in Proset \land A \subseteq B) \to K ↾_{𝑠} A \in Proset$

Metamath Proof Explorer

Theorem ressprs

Proof