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

Metamath Proof Explorer

Theorem paddasslem6

Description: Lemma for paddass . (Contributed by NM, 8-Jan-2012)

		Ref	Expression
	Hypotheses	paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
		paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
		paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	Assertion	paddasslem6	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		paddasslem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		paddasslem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		paddasslem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝐾 ∈ HL )
5		simpl2r	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑠 ∈ 𝐴 )
6		simpl2l	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ∈ 𝐴 )
7		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑧 ∈ 𝐴 )
8	5 6 7	3jca	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → ( 𝑠 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) )
9		simprl	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑠 ≠ 𝑧 )
10	4 8 9	3jca	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → ( 𝐾 ∈ HL ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑠 ≠ 𝑧 ) )
11		simprr	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) )
12	1 2 3	hlatexch2	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑠 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑠 ≠ 𝑧 ) → ( 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) ) )
13	10 11 12	sylc	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) ∧ ( 𝑠 ≠ 𝑧 ∧ 𝑠 ≤ ( 𝑝 ∨ 𝑧 ) ) ) → 𝑝 ≤ ( 𝑠 ∨ 𝑧 ) )