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

Metamath Proof Explorer

Theorem cvrcmp2

Description: If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012)

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

Proof

Step Hyp Ref Expression
1 cvrcmp.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrcmp.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrcmp.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 opposet ⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
5 4 3ad2ant1 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ Poset )
6 simp1 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝐾 ∈ OP )
7 simp22 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑌 ∈ 𝐵 )
8 eqid ⊢ ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 1 8 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
10 6 7 9 syl2anc ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
11 simp21 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑋 ∈ 𝐵 )
12 1 8 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
13 6 11 12 syl2anc ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
14 simp23 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → 𝑍 ∈ 𝐵 )
15 1 8 opoccl ⊢ ( ( 𝐾 ∈ OP ∧ 𝑍 ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 )
16 6 14 15 syl2anc ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 )
17 1 8 3 cvrcon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
18 17 3adant3r2 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
19 1 8 3 cvrcon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
20 19 3adant3r1 ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 𝐶 𝑍 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
21 18 20 anbi12d ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
22 21 biimp3a ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
23 22 ancomd ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
24 1 2 3 cvrcmp ⊢ ( ( 𝐾 ∈ Poset ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) ∈ 𝐵 ) ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑍 ) 𝐶 ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
25 5 10 13 16 23 24 syl131anc ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
26 1 2 8 oplecon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ≤ 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
27 6 11 7 26 syl3anc ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ≤ 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ≤ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
28 1 8 opcon3b ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 = 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
29 6 11 7 28 syl3anc ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 = 𝑌 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) = ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ) )
30 25 27 29 3bitr4d ⊢ ( ( 𝐾 ∈ OP ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝑋 𝐶 𝑍 ∧ 𝑌 𝐶 𝑍 ) ) → ( 𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌 ) )