Theorem isposi

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

	Ref	Expression
Hypotheses	isposi.k	⊢ 𝐾 ∈ V
	isposi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	isposi.l	⊢ ≤ = ( le ‘ 𝐾 )
	isposi.1	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥 )
	isposi.2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
	isposi.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
Assertion	isposi	⊢ 𝐾 ∈ Poset

Proof

Step	Hyp	Ref	Expression
1		isposi.k	⊢ 𝐾 ∈ V
2		isposi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
3		isposi.l	⊢ ≤ = ( le ‘ 𝐾 )
4		isposi.1	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ≤ 𝑥 )
5		isposi.2	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
6		isposi.3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
7	4	3ad2ant1	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → 𝑥 ≤ 𝑥 )
8	5	3adant3	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
9	7 8 6	3jca	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) )
10	9	rgen3	⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
11	2 3	ispos	⊢ ( 𝐾 ∈ Poset ↔ ( 𝐾 ∈ V ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑥 ≤ 𝑥 ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) ∧ ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) ) ) )
12	1 10 11	mpbir2an	⊢ 𝐾 ∈ Poset