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

Metamath Proof Explorer

Theorem cvrletrN

Description: Property of an element above a covering. (Contributed by NM, 7-Dec-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cvrletr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
cvrletr.l ⊢ ≤ = ( le ‘ 𝐾 )
cvrletr.s ⊢ < = ( lt ‘ 𝐾 )
cvrletr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion cvrletrN ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 < 𝑍 ) )

Proof

Step Hyp Ref Expression
1 cvrletr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 cvrletr.l ⊢ ≤ = ( le ‘ 𝐾 )
3 cvrletr.s ⊢ < = ( lt ‘ 𝐾 )
4 cvrletr.c ⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5 simpll ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → 𝐾 ∈ Poset )
6 simplr1 ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 ∈ 𝐵 )
7 simplr2 ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → 𝑌 ∈ 𝐵 )
8 simpr ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 𝐶 𝑌 )
9 1 3 4 cvrlt ⊢ ( ( ( 𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
10 5 6 7 8 9 syl31anc ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → 𝑋 < 𝑌 )
11 1 2 3 pltletr ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 < 𝑍 ) )
12 11 adantr ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → ( ( 𝑋 < 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 < 𝑍 ) )
13 10 12 mpand ⊢ ( ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ 𝑋 𝐶 𝑌 ) → ( 𝑌 ≤ 𝑍 → 𝑋 < 𝑍 ) )
14 13 expimpd ⊢ ( ( 𝐾 ∈ Poset ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝑋 𝐶 𝑌 ∧ 𝑌 ≤ 𝑍 ) → 𝑋 < 𝑍 ) )