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

Metamath Proof Explorer

Theorem ncvr1

Description: No element covers the lattice unity. (Contributed by NM, 8-Jul-2013)

Ref Expression
Hypotheses ncvr1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ncvr1.u ⊢ 1 = ( 1. ‘ 𝐾 )
ncvr1.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion ncvr1 ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ¬ 1 𝐶 𝑋 )

Proof

Step Hyp Ref Expression
1 ncvr1.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 ncvr1.u ⊢ 1 = ( 1. ‘ 𝐾 )
3 ncvr1.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
4 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
5 1 4 2 ople1 ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → 𝑋 ( le ‘ 𝐾 ) 1 )
6 opposet ⊢ ( 𝐾 ∈ OP → 𝐾 ∈ Poset )
7 6 ad2antrr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 ( lt ‘ 𝐾 ) 𝑋 ) → 𝐾 ∈ Poset )
8 1 2 op1cl ⊢ ( 𝐾 ∈ OP → 1 ∈ 𝐵 )
9 8 ad2antrr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 ( lt ‘ 𝐾 ) 𝑋 ) → 1 ∈ 𝐵 )
10 simplr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 ( lt ‘ 𝐾 ) 𝑋 ) → 𝑋 ∈ 𝐵 )
11 simpr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 ( lt ‘ 𝐾 ) 𝑋 ) → 1 ( lt ‘ 𝐾 ) 𝑋 )
12 eqid ⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
13 1 4 12 pltnle ⊢ ( ( ( 𝐾 ∈ Poset ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 1 ( lt ‘ 𝐾 ) 𝑋 ) → ¬ 𝑋 ( le ‘ 𝐾 ) 1 )
14 7 9 10 11 13 syl31anc ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 ( lt ‘ 𝐾 ) 𝑋 ) → ¬ 𝑋 ( le ‘ 𝐾 ) 1 )
15 14 ex ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ( 1 ( lt ‘ 𝐾 ) 𝑋 → ¬ 𝑋 ( le ‘ 𝐾 ) 1 ) )
16 5 15 mt2d ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ¬ 1 ( lt ‘ 𝐾 ) 𝑋 )
17 simpll ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 𝐶 𝑋 ) → 𝐾 ∈ OP )
18 8 ad2antrr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 𝐶 𝑋 ) → 1 ∈ 𝐵 )
19 simplr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 𝐶 𝑋 ) → 𝑋 ∈ 𝐵 )
20 simpr ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 𝐶 𝑋 ) → 1 𝐶 𝑋 )
21 1 12 3 cvrlt ⊢ ( ( ( 𝐾 ∈ OP ∧ 1 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ) ∧ 1 𝐶 𝑋 ) → 1 ( lt ‘ 𝐾 ) 𝑋 )
22 17 18 19 20 21 syl31anc ⊢ ( ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) ∧ 1 𝐶 𝑋 ) → 1 ( lt ‘ 𝐾 ) 𝑋 )
23 16 22 mtand ⊢ ( ( 𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ) → ¬ 1 𝐶 𝑋 )