Theorem 4atexlemv

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	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
	4thatlem0.v	⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
Assertion	4atexlemv	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )

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		4thatlem0.v	⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
9	1	4atexlemk	⊢ ( 𝜑 → 𝐾 ∈ HL )
10	1	4atexlemw	⊢ ( 𝜑 → 𝑊 ∈ 𝐻 )
11	1	4atexlempw	⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) )
12	1	4atexlems	⊢ ( 𝜑 → 𝑆 ∈ 𝐴 )
13	1 2 3 5	4atexlempns	⊢ ( 𝜑 → 𝑃 ≠ 𝑆 )
14	2 3 4 5 6 8	lhpat2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑆 ∈ 𝐴 ∧ 𝑃 ≠ 𝑆 ) ) → 𝑉 ∈ 𝐴 )
15	9 10 11 12 13 14	syl212anc	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )