This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑍 𝐶 𝑋 ∧ 𝑍 𝐶 𝑌 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )