Theorem posasymb

Description: A poset ordering is asymmetric. (Contributed by NM, 21-Oct-2011)

	Ref	Expression
Hypotheses	posi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	posi.l	⊢ ≤ = ( le ‘ 𝐾 )
Assertion	posasymb	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		posi.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		posi.l	⊢ ≤ = ( le ‘ 𝐾 )
3		simp1	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ Poset )
4		simp2	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
5		simp3	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
6	1 2	posi	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) ) )
7	3 4 5 5 6	syl13anc	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑋 ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) ∧ ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 ) ) )
8	7	simp2d	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) → 𝑋 = 𝑌 ) )
9	1 2	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
10		breq2	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑌 ) )
11	9 10	syl5ibcom	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 = 𝑌 → 𝑋 ≤ 𝑌 ) )
12		breq1	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑌 ≤ 𝑋 ) )
13	9 12	syl5ibcom	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 = 𝑌 → 𝑌 ≤ 𝑋 ) )
14	11 13	jcad	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ) )
15	14	3adant3	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ) )
16	8 15	impbid	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )