Theorem posrasymb

Description: A poset ordering is asymmetric. (Contributed by Thierry Arnoux, 13-Sep-2018)

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

Proof

Step	Hyp	Ref	Expression
1		posrasymb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		posrasymb.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3	2	breqi	⊢ ( 𝑋 ≤ 𝑌 ↔ 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 )
4		simp2	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
5		simp3	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
6		brxp	⊢ ( 𝑋 ( 𝐵 × 𝐵 ) 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
7	4 5 6	sylanbrc	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ( 𝐵 × 𝐵 ) 𝑌 )
8		brin	⊢ ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑋 ( 𝐵 × 𝐵 ) 𝑌 ) )
9	8	rbaib	⊢ ( 𝑋 ( 𝐵 × 𝐵 ) 𝑌 → ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
10	7 9	syl	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑌 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
11	3 10	bitrid	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 ( le ‘ 𝐾 ) 𝑌 ) )
12	2	breqi	⊢ ( 𝑌 ≤ 𝑋 ↔ 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 )
13		brxp	⊢ ( 𝑌 ( 𝐵 × 𝐵 ) 𝑋 ↔ ( 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) )
14	5 4 13	sylanbrc	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ( 𝐵 × 𝐵 ) 𝑋 )
15		brin	⊢ ( 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ↔ ( 𝑌 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑌 ( 𝐵 × 𝐵 ) 𝑋 ) )
16	15	rbaib	⊢ ( 𝑌 ( 𝐵 × 𝐵 ) 𝑋 → ( 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ↔ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) )
17	14 16	syl	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) 𝑋 ↔ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) )
18	12 17	bitrid	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ≤ 𝑋 ↔ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) )
19	11 18	anbi12d	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) ) )
20		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
21	1 20	posasymb	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ( le ‘ 𝐾 ) 𝑌 ∧ 𝑌 ( le ‘ 𝐾 ) 𝑋 ) ↔ 𝑋 = 𝑌 ) )
22	19 21	bitrd	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ≤ 𝑌 ∧ 𝑌 ≤ 𝑋 ) ↔ 𝑋 = 𝑌 ) )