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)

	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		df-ple	⊢ le = Slot ; 1 0
10		1lt10	⊢ 1 < ; 1 0
11		10nn	⊢ ; 1 0 ∈ ℕ
12	3 9 10 11	2strbas	⊢ ( 𝐵 ∈ V → 𝐵 = ( Base ‘ 𝐾 ) )
13	1 12	ax-mp	⊢ 𝐵 = ( Base ‘ 𝐾 )
14	3 9 10 11	2strop	⊢ ( ≤ ∈ V → ≤ = ( le ‘ 𝐾 ) )
15	2 14	ax-mp	⊢ ≤ = ( le ‘ 𝐾 )
16	8 13 15 4 5 6	isposi	⊢ 𝐾 ∈ Poset