Theorem 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	⊢ 𝐵 ∈ V
	isposix.b	⊢ ≤ ∈ V
	isposix.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ }
	isposix.1	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥 )
	isposix.2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
	isposix.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
Assertion	isposix	⊢ 𝐾 ∈ Poset

Proof

Step	Hyp	Ref	Expression
1		isposix.a	⊢ 𝐵 ∈ V
2		isposix.b	⊢ ≤ ∈ V
3		isposix.k	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ }
4		isposix.1	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥 )
5		isposix.2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
6		isposix.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
7		prex	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } ∈ V
8	3 7	eqeltri	⊢ 𝐾 ∈ V
9		basendxltplendx	⊢ ( Base ‘ ndx ) < ( le ‘ ndx )
10		plendxnn	⊢ ( le ‘ ndx ) ∈ ℕ
11	3 9 10	2strbas1	⊢ ( 𝐵 ∈ V → 𝐵 = ( Base ‘ 𝐾 ) )
12	1 11	ax-mp	⊢ 𝐵 = ( Base ‘ 𝐾 )
13		pleid	⊢ le = Slot ( le ‘ ndx )
14	3 9 10 13	2strop1	⊢ ( ≤ ∈ V → ≤ = ( le ‘ 𝐾 ) )
15	2 14	ax-mp	⊢ ≤ = ( le ‘ 𝐾 )
16	8 12 15 4 5 6	isposi	⊢ 𝐾 ∈ Poset