isposix

Description: Properties that determine a poset (explicit structure version). Note that the numeric indices of the structure components are not mentioned explicitly in either the theorem or its proof. (Contributed by NM, 9-Nov-2012) (Proof shortened by AV, 30-Oct-2024)

	Ref	Expression
Hypotheses	isposix.a	$⊢ B \in V$
	isposix.b	$⊢ \underset{˙}{\leq} \in V$
	isposix.k	$⊢ K = \{⟨{Base}_{ndx}, B⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\}$
	isposix.1	$⊢ x \in B \to x \underset{˙}{\leq} x$
	isposix.2	$⊢ (x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
	isposix.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	isposix	$⊢ K \in Poset$

Proof

Step	Hyp	Ref	Expression
1		isposix.a	$⊢ B \in V$
2		isposix.b	$⊢ \underset{˙}{\leq} \in V$
3		isposix.k	$⊢ K = \{⟨{Base}_{ndx}, B⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\}$
4		isposix.1	$⊢ x \in B \to x \underset{˙}{\leq} x$
5		isposix.2	$⊢ (x \in B \land y \in B) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
6		isposix.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		prex	$⊢ \{⟨{Base}_{ndx}, B⟩, ⟨\leq_{ndx}, \underset{˙}{\leq}⟩\} \in V$
8	3 7	eqeltri	$⊢ K \in V$
9		basendxltplendx	$⊢ {Base}_{ndx} < \leq_{ndx}$
10		plendxnn	$⊢ \leq_{ndx} \in ℕ$
11	3 9 10	2strbas	$⊢ B \in V \to B = {Base}_{K}$
12	1 11	ax-mp	$⊢ B = {Base}_{K}$
13		pleid	$⊢ le = Slot \leq_{ndx}$
14	3 9 10 13	2strop	$⊢ \underset{˙}{\leq} \in V \to \underset{˙}{\leq} = \leq_{K}$
15	2 14	ax-mp	$⊢ \underset{˙}{\leq} = \leq_{K}$
16	8 12 15 4 5 6	isposi	$⊢ K \in Poset$

Metamath Proof Explorer

Theorem isposix

Proof