isposi

Description: Properties that determine a poset (implicit structure version). (Contributed by NM, 11-Sep-2011)

	Ref	Expression
Hypotheses	isposi.k	$⊢ K \in V$
	isposi.b	$⊢ B = {Base}_{K}$
	isposi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	isposi.1	$⊢ x \in B \to x \underset{˙}{\leq} x$
	isposi.2	$⊢ (x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
	isposi.3	$⊢ (x \in B \land y \in B \land z \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
Assertion	isposi	$⊢ K \in Poset$

Step	Hyp	Ref	Expression
1		isposi.k	$⊢ K \in V$
2		isposi.b	$⊢ B = {Base}_{K}$
3		isposi.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
4		isposi.1	$⊢ x \in B \to x \underset{˙}{\leq} x$
5		isposi.2	$⊢ (x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
6		isposi.3	$⊢ (x \in B \land y \in B \land z \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
7	4	3ad2ant1	$⊢ (x \in B \land y \in B \land z \in B) \to x \underset{˙}{\leq} x$
8	5	3adant3	$⊢ (x \in B \land y \in B \land z \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
9	7 8 6	3jca	$⊢ (x \in B \land y \in B \land z \in B) \to (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))$
10	9	rgen3	$⊢ \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))$
11	2 3	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)))$
12	1 10 11	mpbir2an	$⊢ K \in Poset$

Metamath Proof Explorer