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