oduprs

Description: Being a proset is a self-dual property. (Contributed by Thierry Arnoux, 13-Sep-2018)

		Ref	Expression
	Hypothesis	oduprs.d	$⊢ D = ODual (K)$
	Assertion	oduprs	$⊢ K \in Proset \to D \in Proset$

Proof

Step	Hyp	Ref	Expression
1		oduprs.d	$⊢ D = ODual (K)$
2		eqid	$⊢ {Base}_{K} = {Base}_{K}$
3		eqid	$⊢ \leq_{K} = \leq_{K}$
4	2 3	isprs	$⊢ K \in Proset \leftrightarrow (K \in V \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z)))$
5	4	simprbi	$⊢ K \in Proset \to \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
6	5	r19.21bi	$⊢ (K \in Proset \land x \in {Base}_{K}) \to \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
7	6	r19.21bi	$⊢ ((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \to \forall z \in {Base}_{K} (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
8	7	r19.21bi	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \land z \in {Base}_{K}) \to (x \leq_{K} x \land ((x \leq_{K} y \land y \leq_{K} z) \to x \leq_{K} z))$
9	8	simpld	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \land z \in {Base}_{K}) \to x \leq_{K} x$
10		vex	$⊢ x \in V$
11	10 10	brcnv	$⊢ x {\leq_{K}}^{-1} x \leftrightarrow x \leq_{K} x$
12	9 11	sylibr	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \land z \in {Base}_{K}) \to x {\leq_{K}}^{-1} x$
13	2 3	isprs	$⊢ K \in Proset \leftrightarrow (K \in V \land \forall z \in {Base}_{K} \forall y \in {Base}_{K} \forall x \in {Base}_{K} (z \leq_{K} z \land ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x)))$
14	13	simprbi	$⊢ K \in Proset \to \forall z \in {Base}_{K} \forall y \in {Base}_{K} \forall x \in {Base}_{K} (z \leq_{K} z \land ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x))$
15	14	r19.21bi	$⊢ (K \in Proset \land z \in {Base}_{K}) \to \forall y \in {Base}_{K} \forall x \in {Base}_{K} (z \leq_{K} z \land ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x))$
16	15	r19.21bi	$⊢ ((K \in Proset \land z \in {Base}_{K}) \land y \in {Base}_{K}) \to \forall x \in {Base}_{K} (z \leq_{K} z \land ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x))$
17	16	r19.21bi	$⊢ (((K \in Proset \land z \in {Base}_{K}) \land y \in {Base}_{K}) \land x \in {Base}_{K}) \to (z \leq_{K} z \land ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x))$
18	17	simprd	$⊢ (((K \in Proset \land z \in {Base}_{K}) \land y \in {Base}_{K}) \land x \in {Base}_{K}) \to ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x)$
19	18	an32s	$⊢ (((K \in Proset \land z \in {Base}_{K}) \land x \in {Base}_{K}) \land y \in {Base}_{K}) \to ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x)$
20	19	ex	$⊢ ((K \in Proset \land z \in {Base}_{K}) \land x \in {Base}_{K}) \to (y \in {Base}_{K} \to ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x))$
21	20	an32s	$⊢ ((K \in Proset \land x \in {Base}_{K}) \land z \in {Base}_{K}) \to (y \in {Base}_{K} \to ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x))$
22	21	imp	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land z \in {Base}_{K}) \land y \in {Base}_{K}) \to ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x)$
23	22	an32s	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \land z \in {Base}_{K}) \to ((z \leq_{K} y \land y \leq_{K} x) \to z \leq_{K} x)$
24		vex	$⊢ y \in V$
25	10 24	brcnv	$⊢ x {\leq_{K}}^{-1} y \leftrightarrow y \leq_{K} x$
26		vex	$⊢ z \in V$
27	24 26	brcnv	$⊢ y {\leq_{K}}^{-1} z \leftrightarrow z \leq_{K} y$
28	25 27	anbi12ci	$⊢ (x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \leftrightarrow (z \leq_{K} y \land y \leq_{K} x)$
29	10 26	brcnv	$⊢ x {\leq_{K}}^{-1} z \leftrightarrow z \leq_{K} x$
30	23 28 29	3imtr4g	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \land z \in {Base}_{K}) \to ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z)$
31	12 30	jca	$⊢ (((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \land z \in {Base}_{K}) \to (x {\leq_{K}}^{-1} x \land ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z))$
32	31	ralrimiva	$⊢ ((K \in Proset \land x \in {Base}_{K}) \land y \in {Base}_{K}) \to \forall z \in {Base}_{K} (x {\leq_{K}}^{-1} x \land ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z))$
33	32	ralrimiva	$⊢ (K \in Proset \land x \in {Base}_{K}) \to \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x {\leq_{K}}^{-1} x \land ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z))$
34	33	ralrimiva	$⊢ K \in Proset \to \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x {\leq_{K}}^{-1} x \land ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z))$
35	1	fvexi	$⊢ D \in V$
36	34 35	jctil	$⊢ K \in Proset \to (D \in V \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x {\leq_{K}}^{-1} x \land ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z)))$
37	1 2	odubas	$⊢ {Base}_{K} = {Base}_{D}$
38	1 3	oduleval	$⊢ {\leq_{K}}^{-1} = \leq_{D}$
39	37 38	isprs	$⊢ D \in Proset \leftrightarrow (D \in V \land \forall x \in {Base}_{K} \forall y \in {Base}_{K} \forall z \in {Base}_{K} (x {\leq_{K}}^{-1} x \land ((x {\leq_{K}}^{-1} y \land y {\leq_{K}}^{-1} z) \to x {\leq_{K}}^{-1} z)))$
40	36 39	sylibr	$⊢ K \in Proset \to D \in Proset$

Metamath Proof Explorer

Theorem oduprs

Proof