ispos

Description: The predicate "is a poset". (Contributed by NM, 18-Oct-2012) (Revised by Mario Carneiro, 4-Nov-2013)

	Ref	Expression
Hypotheses	ispos.b	$⊢ B = {Base}_{K}$
	ispos.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
Assertion	ispos	$⊢ K \in Poset \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$

Proof

Step	Hyp	Ref	Expression
1		ispos.b	$⊢ B = {Base}_{K}$
2		ispos.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		fveq2	$⊢ p = K \to {Base}_{p} = {Base}_{K}$
4	3 1	eqtr4di	$⊢ p = K \to {Base}_{p} = B$
5	4	eqeq2d	$⊢ p = K \to (b = {Base}_{p} \leftrightarrow b = B)$
6		fveq2	$⊢ p = K \to \leq_{p} = \leq_{K}$
7	6 2	eqtr4di	$⊢ p = K \to \leq_{p} = \underset{˙}{\leq}$
8	7	eqeq2d	$⊢ p = K \to (r = \leq_{p} \leftrightarrow r = \underset{˙}{\leq})$
9	5 8	3anbi12d	$⊢ p = K \to ((b = {Base}_{p} \land r = \leq_{p} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))) \leftrightarrow (b = B \land r = \underset{˙}{\leq} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))))$
10	9	2exbidv	$⊢ p = K \to (\exists b \exists r (b = {Base}_{p} \land r = \leq_{p} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))) \leftrightarrow \exists b \exists r (b = B \land r = \underset{˙}{\leq} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))))$
11		df-poset	$⊢ Poset = \{p \| \exists b \exists r (b = {Base}_{p} \land r = \leq_{p} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))\}$
12	10 11	elab4g	$⊢ K \in Poset \leftrightarrow (K \in V \land \exists b \exists r (b = B \land r = \underset{˙}{\leq} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z))))$
13	1	fvexi	$⊢ B \in V$
14	2	fvexi	$⊢ \underset{˙}{\leq} \in V$
15		raleq	$⊢ b = B \to (\forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \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 x) \to x = y) \land ((x r y \land y r z) \to x r z)))$
16	15	raleqbi1dv	$⊢ b = B \to (\forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \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 x) \to x = y) \land ((x r y \land y r z) \to x r z)))$
17	16	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 x) \to x = y) \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 x) \to x = y) \land ((x r y \land y r z) \to x r z)))$
18		breq	$⊢ r = \underset{˙}{\leq} \to (x r x \leftrightarrow x \underset{˙}{\leq} x)$
19		breq	$⊢ r = \underset{˙}{\leq} \to (x r y \leftrightarrow x \underset{˙}{\leq} y)$
20		breq	$⊢ r = \underset{˙}{\leq} \to (y r x \leftrightarrow y \underset{˙}{\leq} x)$
21	19 20	anbi12d	$⊢ r = \underset{˙}{\leq} \to ((x r y \land y r x) \leftrightarrow (x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x))$
22	21	imbi1d	$⊢ r = \underset{˙}{\leq} \to (((x r y \land y r x) \to x = y) \leftrightarrow ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y))$
23		breq	$⊢ r = \underset{˙}{\leq} \to (y r z \leftrightarrow y \underset{˙}{\leq} z)$
24	19 23	anbi12d	$⊢ r = \underset{˙}{\leq} \to ((x r y \land y r z) \leftrightarrow (x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z))$
25		breq	$⊢ r = \underset{˙}{\leq} \to (x r z \leftrightarrow x \underset{˙}{\leq} z)$
26	24 25	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))$
27	18 22 26	3anbi123d	$⊢ r = \underset{˙}{\leq} \to ((x r x \land ((x r y \land y r x) \to x = y) \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
28	27	ralbidv	$⊢ r = \underset{˙}{\leq} \to (\forall z \in B (x r x \land ((x r y \land y r x) \to x = y) \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
29	28	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 x) \to x = y) \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
30	13 14 17 29	ceqsex2v	$⊢ \exists b \exists r (b = B \land r = \underset{˙}{\leq} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z))$
31	30	anbi2i	$⊢ (K \in V \land \exists b \exists r (b = B \land r = \underset{˙}{\leq} \land \forall x \in b \forall y \in b \forall z \in b (x r x \land ((x r y \land y r x) \to x = y) \land ((x r y \land y r z) \to x r z)))) \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$
32	12 31	bitri	$⊢ K \in Poset \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} x) \to x = y) \land ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)))$

Metamath Proof Explorer

Theorem ispos

Proof