Theorem 4atexlemu

Description: Lemma for 4atexlem7 . (Contributed by NM, 23-Nov-2012)

	Ref	Expression
Hypotheses	4thatlem.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
	4thatlem0.l	⊢ ≤ = ( le ‘ 𝐾 )
	4thatlem0.j	⊢ ∨ = ( join ‘ 𝐾 )
	4thatlem0.m	⊢ ∧ = ( meet ‘ 𝐾 )
	4thatlem0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	4thatlem0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	4thatlem0.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
Assertion	4atexlemu	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		4thatlem.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
2		4thatlem0.l	⊢ ≤ = ( le ‘ 𝐾 )
3		4thatlem0.j	⊢ ∨ = ( join ‘ 𝐾 )
4		4thatlem0.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		4thatlem0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		4thatlem0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		4thatlem0.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8	1	4atexlemk	⊢ ( 𝜑 → 𝐾 ∈ HL )
9	1	4atexlemw	⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
10	1	4atexlempw	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
11	1	4atexlemq	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
12	1	4atexlempnq	⊢ ( 𝜑 → 𝑃 ≠ 𝑄 )
13	2 3 4 5 6 7	lhpat2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄 ) ) → 𝑈 ∈ 𝐴 )
14	8 9 10 11 12 13	syl212anc	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )