Theorem cvrcmp

Description: If two lattice elements that cover a third are comparable, then they are equal. (Contributed by NM, 6-Feb-2012)

	Ref	Expression
Hypotheses	cvrcmp.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrcmp.l	⊢ ≤ = ( le ‘ 𝐾 )
	cvrcmp.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	cvrcmp	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		cvrcmp.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrcmp.l	⊢ ≤ = ( le ‘ 𝐾 )
3		cvrcmp.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4		simpl1	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝐾 ∈ Poset )
5		simpl23	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑍 ∈ 𝐵 )
6		simpl21	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ∈ 𝐵 )
7		simpl3l	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑍 𝐶 𝑋 )
8	1 3	cvrne	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 𝐶 𝑋 ) → 𝑍 ≠ 𝑋 )
9	4 5 6 7 8	syl31anc	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑍 ≠ 𝑋 )
10	1 2 3	cvrle	⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑍 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 𝐶 𝑋 ) → 𝑍 ≤ 𝑋 )
11	4 5 6 7 10	syl31anc	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑍 ≤ 𝑋 )
12		simpr	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 ≤ 𝑌 )
13		simpl22	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑌 ∈ 𝐵 )
14		simpl3r	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑍 𝐶 𝑌 )
15	1 2 3	cvrnbtwn4	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑍 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑍 𝐶 𝑌 ) → ( ( 𝑍 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ↔ ( 𝑍 = 𝑋 ∨ 𝑋 = 𝑌 ) ) )
16	4 5 13 6 14 15	syl131anc	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( ( 𝑍 ≤ 𝑋 ∧ 𝑋 ≤ 𝑌 ) ↔ ( 𝑍 = 𝑋 ∨ 𝑋 = 𝑌 ) ) )
17	11 12 16	mpbi2and	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑍 = 𝑋 ∨ 𝑋 = 𝑌 ) )
18		neor	⊢ ( ( 𝑍 = 𝑋 ∨ 𝑋 = 𝑌 ) ↔ ( 𝑍 ≠ 𝑋 → 𝑋 = 𝑌 ) )
19	17 18	sylib	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → ( 𝑍 ≠ 𝑋 → 𝑋 = 𝑌 ) )
20	9 19	mpd	⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) ∧ 𝑋 ≤ 𝑌 ) → 𝑋 = 𝑌 )
21	20	ex	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → ( 𝑋 ≤ 𝑌 → 𝑋 = 𝑌 ) )
22		simp1	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → 𝐾 ∈ Poset )
23		simp21	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → 𝑋 ∈ 𝐵 )
24	1 2	posref	⊢ ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ≤ 𝑋 )
25	22 23 24	syl2anc	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → 𝑋 ≤ 𝑋 )
26		breq2	⊢ ( 𝑋 = 𝑌 → ( 𝑋 ≤ 𝑋 ↔ 𝑋 ≤ 𝑌 ) )
27	25 26	syl5ibcom	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → ( 𝑋 = 𝑌 → 𝑋 ≤ 𝑌 ) )
28	21 27	impbid	⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )