isprs

Description: Property of being a preordered set. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypotheses	isprs.b	$⊢ B = {Base}_{K}$
	isprs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
Assertion	isprs	$⊢ K \in Proset \leftrightarrow (K \in V \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$

Proof

Step	Hyp	Ref	Expression
1		isprs.b	$⊢ B = {Base}_{K}$
2		isprs.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		fveq2	$⊢ f = K \to {Base}_{f} = {Base}_{K}$
4		fveq2	$⊢ f = K \to \leq_{f} = \leq_{K}$
5	4	sbceq1d	$⊢ f = K \to (\underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \underset{˙}{[} \leq_{K} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)))$
6	3 5	sbceqbid	$⊢ f = K \to (\underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \underset{˙}{[} {Base}_{K} / b \underset{˙}{]} \underset{˙}{[} \leq_{K} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)))$
7		fvex	$⊢ {Base}_{K} \in V$
8		fvex	$⊢ \leq_{K} \in V$
9		eqtr3	$⊢ (b = {Base}_{K} \land B = {Base}_{K}) \to b = B$
10	1 9	mpan2	$⊢ b = {Base}_{K} \to b = B$
11		raleq	$⊢ b = B \to (\forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall z \in B (x r x \land ((x r y \land y r z) \to x r z)))$
12	11	raleqbi1dv	$⊢ b = B \to (\forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall y \in B \forall z \in B (x r x \land ((x r y \land y r z) \to x r z)))$
13	12	raleqbi1dv	$⊢ b = B \to (\forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x r x \land ((x r y \land y r z) \to x r z)))$
14	10 13	syl	$⊢ b = {Base}_{K} \to (\forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x r x \land ((x r y \land y r z) \to x r z)))$
15		eqtr3	$⊢ (r = \leq_{K} \land \underset{˙}{\leq} = \leq_{K}) \to r = \underset{˙}{\leq}$
16	2 15	mpan2	$⊢ r = \leq_{K} \to r = \underset{˙}{\leq}$
17		breq	$⊢ r = \underset{˙}{\leq} \to (x r x \leftrightarrow x \underset{˙}{\leq} x)$
18		breq	$⊢ r = \underset{˙}{\leq} \to (x r y \leftrightarrow x \underset{˙}{\leq} y)$
19		breq	$⊢ r = \underset{˙}{\leq} \to (y r z \leftrightarrow y \underset{˙}{\leq} z)$
20	18 19	anbi12d	$⊢ r = \underset{˙}{\leq} \to ((x r y \land y r z) \leftrightarrow (x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z))$
21		breq	$⊢ r = \underset{˙}{\leq} \to (x r z \leftrightarrow x \underset{˙}{\leq} z)$
22	20 21	imbi12d	$⊢ r = \underset{˙}{\leq} \to (((x r y \land y r z) \to x r z) \leftrightarrow ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))$
23	17 22	anbi12d	$⊢ r = \underset{˙}{\leq} \to ((x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
24	23	ralbidv	$⊢ r = \underset{˙}{\leq} \to (\forall z \in B (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
25	24	2ralbidv	$⊢ r = \underset{˙}{\leq} \to (\forall x \in B \forall y \in B \forall z \in B (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
26	16 25	syl	$⊢ r = \leq_{K} \to (\forall x \in B \forall y \in B \forall z \in B (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
27	14 26	sylan9bb	$⊢ (b = {Base}_{K} \land r = \leq_{K}) \to (\forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
28	7 8 27	sbc2ie	$⊢ \underset{˙}{[} {Base}_{K} / b \underset{˙}{]} \underset{˙}{[} \leq_{K} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))$
29	6 28	bitrdi	$⊢ f = K \to (\underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z)) \leftrightarrow \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
30		df-proset	$⊢ Proset = \{f \| \underset{˙}{[} {Base}_{f} / b \underset{˙}{]} \underset{˙}{[} \leq_{f} / r \underset{˙}{]} \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r z) \to x r z))\}$
31	29 30	elab4g	$⊢ K \in Proset \leftrightarrow (K \in V \land \forall x \in B \forall y \in B \forall z \in B (x \underset{˙}{\leq} x \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$

Metamath Proof Explorer

Theorem isprs

Proof